Theorem vtoclga 3262

Description: Implicit substitution of a class for a setvar variable. (Contributed by NM, 20-Aug-1995.)

Hypotheses

Ref	Expression
vtoclga.1	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
vtoclga.2	⊢ (𝑥 ∈ 𝐵 → 𝜑)

Assertion

Ref	Expression
vtoclga	⊢ (𝐴 ∈ 𝐵 → 𝜓)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝜓,𝑥

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem vtoclga

Step	Hyp	Ref	Expression
1		nfcv 2761	. 2 ⊢ Ⅎ𝑥𝐴
2		nfv 1840	. 2 ⊢ Ⅎ𝑥𝜓
3		vtoclga.1	. 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
4		vtoclga.2	. 2 ⊢ (𝑥 ∈ 𝐵 → 𝜑)
5	1, 2, 3, 4	vtoclgaf 3261	1 ⊢ (𝐴 ∈ 𝐵 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 196   = wceq 1480   ∈ wcel 1987

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-v 3192

This theorem is referenced by:  vtoclri  3273  ssuniOLD  4433  disjxiun  4619  disjxiunOLD  4620  wfis3  5690  opabiota  6228  fvmpt3  6253  fvmptss  6259  fnressn  6390  fressnfv  6392  caovord  6810  caovmo  6836  ordunisuc  6994  tfis3  7019  wfr2a  7392  onfununi  7398  smogt  7424  tz7.44-1  7462  tz7.44-2  7463  tz7.44-3  7464  nnacl  7651  nnmcl  7652  nnecl  7653  nnacom  7657  nnaass  7662  nndi  7663  nnmass  7664  nnmsucr  7665  nnmcom  7666  nnmordi  7671  ixpfn  7874  findcard  8159  findcard2  8160  marypha1  8300  cantnfle  8528  cantnflem1  8546  cnfcom  8557  fseqenlem1  8807  ackbij1lem5  9006  ackbij1lem8  9009  cardcf  9034  cfsmolem  9052  wunex2  9520  ingru  9597  recrecnq  9749  prlem934  9815  nn1suc  11001  uzind4s2  11709  rpnnen1lem6  11779  rpnnen1OLD  11785  cnref1o  11787  xmulasslem  12074  om2uzsuci  12703  expcl2lem  12828  hashmap  13178  hashpw  13179  seqcoll  13202  climub  14342  climserle  14343  sumrblem  14391  fsumcvg  14392  summolem2a  14395  infcvgaux2i  14534  prodfn0  14570  prodfrec  14571  prodrblem  14603  fprodcvg  14604  prodmolem2a  14608  divalglem8  15066  bezoutlem1  15199  alginv  15231  algcvg  15232  algcvga  15235  algfx  15236  isprm2lem  15337  prmind2  15341  prmpwdvds  15551  cnextfvval  21809  xrsxmet  22552  xrhmeo  22685  cmetcaulem  23026  bcth3  23068  itg2addlem  23465  taylfval  24051  sinord  24218  logexprlim  24884  lgsdir2lem4  24987  hlim2  27937  elnlfn  28675  lnconi  28780  chirredlem3  29139  chirredlem4  29140  cnre2csqlem  29780  eulerpartlemsf  30244  eulerpartlemn  30266  bnj1321  30856  bnj1418  30869  subfacp1lem1  30922  frins3  31502  nn0prpwlem  32012  findreccl  32147  mptsnunlem  32856  rdgeqoa  32889  poimirlem22  33102  poimirlem26  33106  mblfinlem3  33119  mblfinlem4  33120  ismblfin  33121  ftc1anclem3  33158  ftc1anclem8  33163  sdclem2  33209  iscringd  33468  renegclALT  33768  zindbi  37030  fmuldfeq  39251  sumnnodd  39298  iblspltprt  39526  stoweidlem2  39556  stoweidlem17  39571  stoweidlem21  39575  stoweidlem43  39597  stoweidlem51  39605  wallispi  39624