Theorem vtoclga 3258

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 3257	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 3188

This theorem is referenced by:  vtoclri  3269  ssuniOLD  4426  disjxiun  4609  disjxiunOLD  4610  wfis3  5680  opabiota  6218  fvmpt3  6243  fvmptss  6249  fnressn  6379  fressnfv  6381  caovord  6798  caovmo  6824  ordunisuc  6979  tfis3  7004  wfr2a  7377  onfununi  7383  smogt  7409  tz7.44-1  7447  tz7.44-2  7448  tz7.44-3  7449  nnacl  7636  nnmcl  7637  nnecl  7638  nnacom  7642  nnaass  7647  nndi  7648  nnmass  7649  nnmsucr  7650  nnmcom  7651  nnmordi  7656  ixpfn  7858  findcard  8143  findcard2  8144  marypha1  8284  cantnfle  8512  cantnflem1  8530  cnfcom  8541  fseqenlem1  8791  ackbij1lem5  8990  ackbij1lem8  8993  cardcf  9018  cfsmolem  9036  wunex2  9504  ingru  9581  recrecnq  9733  prlem934  9799  nn1suc  10985  uzind4s2  11693  rpnnen1lem6  11763  rpnnen1OLD  11769  cnref1o  11771  xmulasslem  12058  om2uzsuci  12687  expcl2lem  12812  hashmap  13162  hashpw  13163  seqcoll  13186  climub  14326  climserle  14327  sumrblem  14375  fsumcvg  14376  summolem2a  14379  infcvgaux2i  14515  prodfn0  14551  prodfrec  14552  prodrblem  14584  fprodcvg  14585  prodmolem2a  14589  divalglem8  15047  bezoutlem1  15180  alginv  15212  algcvg  15213  algcvga  15216  algfx  15217  isprm2lem  15318  prmind2  15322  prmpwdvds  15532  cnextfvval  21779  xrsxmet  22520  xrhmeo  22653  cmetcaulem  22994  bcth3  23036  itg2addlem  23431  taylfval  24017  sinord  24184  logexprlim  24850  lgsdir2lem4  24953  hlim2  27895  elnlfn  28633  lnconi  28738  chirredlem3  29097  chirredlem4  29098  cnre2csqlem  29735  eulerpartlemsf  30199  eulerpartlemn  30221  bnj1321  30800  bnj1418  30813  subfacp1lem1  30866  frins3  31446  nn0prpwlem  31956  findreccl  32091  mptsnunlem  32814  rdgeqoa  32847  poimirlem22  33060  poimirlem26  33064  mblfinlem3  33077  mblfinlem4  33078  ismblfin  33079  ftc1anclem3  33116  ftc1anclem8  33121  sdclem2  33167  iscringd  33426  renegclALT  33726  zindbi  36988  fmuldfeq  39216  sumnnodd  39263  iblspltprt  39493  stoweidlem2  39523  stoweidlem17  39538  stoweidlem21  39542  stoweidlem43  39564  stoweidlem51  39572  wallispi  39591