Theorem vtoclga 3245

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 2751	. 2 ⊢ Ⅎ𝑥𝐴
2		nfv 1830	. 2 ⊢ Ⅎ𝑥𝜓
3		vtoclga.1	. 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
4		vtoclga.2	. 2 ⊢ (𝑥 ∈ 𝐵 → 𝜑)
5	1, 2, 3, 4	vtoclgaf 3244	1 ⊢ (𝐴 ∈ 𝐵 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 195   = wceq 1475   ∈ wcel 1977

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175

This theorem is referenced by:  vtoclri  3256  ssuniOLD  4396  disjxiun  4579  disjxiunOLD  4580  wfis3  5638  opabiota  6171  fvmpt3  6195  fvmptss  6201  fnressn  6330  fressnfv  6332  caovord  6743  caovmo  6769  ordunisuc  6924  tfis3  6949  wfr2a  7319  onfununi  7325  smogt  7351  tz7.44-1  7389  tz7.44-2  7390  tz7.44-3  7391  nnacl  7578  nnmcl  7579  nnecl  7580  nnacom  7584  nnaass  7589  nndi  7590  nnmass  7591  nnmsucr  7592  nnmcom  7593  nnmordi  7598  ixpfn  7800  findcard  8084  findcard2  8085  marypha1  8223  cantnfle  8451  cantnflem1  8469  cnfcom  8480  fseqenlem1  8730  ackbij1lem5  8929  ackbij1lem8  8932  cardcf  8957  cfsmolem  8975  wunex2  9439  ingru  9516  recrecnq  9668  prlem934  9734  nn1suc  10918  uzind4s2  11625  rpnnen1lem6  11695  rpnnen1OLD  11701  cnref1o  11703  xmulasslem  11987  om2uzsuci  12609  expcl2lem  12734  hashmap  13082  hashpw  13083  seqcoll  13105  climub  14240  climserle  14241  sumrblem  14289  fsumcvg  14290  summolem2a  14293  infcvgaux2i  14429  prodfn0  14465  prodfrec  14466  prodrblem  14498  fprodcvg  14499  prodmolem2a  14503  divalglem8  14961  bezoutlem1  15094  alginv  15126  algcvg  15127  algcvga  15130  algfx  15131  isprm2lem  15232  prmind2  15236  prmpwdvds  15446  cnextfvval  21679  xrsxmet  22420  xrhmeo  22553  cmetcaulem  22894  bcth3  22936  itg2addlem  23331  taylfval  23917  sinord  24084  logexprlim  24750  lgsdir2lem4  24853  hlim2  27433  elnlfn  28171  lnconi  28276  chirredlem3  28635  chirredlem4  28636  cnre2csqlem  29284  eulerpartlemsf  29748  eulerpartlemn  29770  bnj1321  30349  bnj1418  30362  subfacp1lem1  30415  frins3  30992  nn0prpwlem  31487  findreccl  31622  mptsnunlem  32361  rdgeqoa  32394  poimirlem22  32601  poimirlem26  32605  mblfinlem3  32618  mblfinlem4  32619  ismblfin  32620  ftc1anclem3  32657  ftc1anclem8  32662  sdclem2  32708  iscringd  32967  renegclALT  33267  zindbi  36529  fmuldfeq  38650  sumnnodd  38697  iblspltprt  38865  stoweidlem2  38895  stoweidlem17  38910  stoweidlem21  38914  stoweidlem43  38936  stoweidlem51  38944  wallispi  38963