Theorem vtoclga 3490

Description: Implicit substitution of a class for a setvar variable. (Contributed by NM, 20-Aug-1995.) Avoid ax-10 2077 and ax-11 2091. (Revised by Gino Giotto, 20-Aug-2023.)

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		eleq1 2850	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
2		vtoclga.1	. . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
3	1, 2	imbi12d 337	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 → 𝜑) ↔ (𝐴 ∈ 𝐵 → 𝜓)))
4		vtoclga.2	. . 3 ⊢ (𝑥 ∈ 𝐵 → 𝜑)
5	3, 4	vtoclg 3483	. 2 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ 𝐵 → 𝜓))
6	5	pm2.43i 52	1 ⊢ (𝐴 ∈ 𝐵 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 198   = wceq 1507   ∈ wcel 2048

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-12 2104  ax-ext 2747

This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1743  df-nf 1747  df-cleq 2768  df-clel 2843

This theorem is referenced by:  vtocl2ga  3491  vtoclri  3501  disjxiun  4924  wfis3  6025  opabiota  6572  fvmpt3  6597  fvmptss  6604  fnressn  6741  fressnfv  6743  caovord  7173  caovmo  7199  ordunisuc  7361  tfis3  7386  wfr2a  7773  onfununi  7779  smogt  7805  tz7.44-1  7843  tz7.44-2  7844  tz7.44-3  7845  nnacl  8034  nnmcl  8035  nnecl  8036  nnacom  8040  nnaass  8045  nndi  8046  nnmass  8047  nnmsucr  8048  nnmcom  8049  nnmordi  8054  ixpfn  8261  findcard  8548  findcard2  8549  marypha1  8689  cantnfle  8924  cantnflem1  8942  cnfcom  8953  fseqenlem1  9240  ackbij1lem8  9443  cardcf  9468  cfsmolem  9486  wunex2  9954  ingru  10031  recrecnq  10183  prlem934  10249  nn1suc  11458  uzind4s2  12120  rpnnen1lem6  12193  cnref1o  12196  xmulasslem  12491  om2uzsuci  13128  expcl2lem  13253  hashpw  13604  seqcoll  13629  climub  14873  climserle  14874  sumrblem  14922  fsumcvg  14923  summolem2a  14926  infcvgaux2i  15067  prodfn0  15104  prodfrec  15105  prodrblem  15137  fprodcvg  15138  prodmolem2a  15142  divalglem8  15605  bezoutlem1  15737  alginv  15769  algcvg  15770  algcvga  15773  algfx  15774  prmind2  15879  prmpwdvds  16090  cnextfvval  22371  xrsxmet  23114  xrhmeo  23247  cmetcaulem  23588  bcth3  23631  itg2addlem  24056  taylfval  24644  sinord  24813  logexprlim  25497  lgsdir2lem4  25600  hlim2  28742  elnlfn  29480  lnconi  29585  chirredlem3  29944  chirredlem4  29945  cnre2csqlem  30788  eulerpartlemsf  31253  eulerpartlemn  31275  bnj1321  31935  bnj1418  31948  subfacp1lem1  32001  frins3  32584  fpr2  32631  frr2  32636  nn0prpwlem  33161  findreccl  33291  mptsnunlem  34026  rdgeqoa  34058  domalom  34091  poimirlem22  34333  poimirlem26  34337  mblfinlem3  34350  mblfinlem4  34351  ismblfin  34352  ftc1anclem3  34388  ftc1anclem8  34393  sdclem2  34437  iscringd  34696  renegclALT  35522  zindbi  38917  fmuldfeq  41274  sumnnodd  41321  iblspltprt  41667  stoweidlem2  41697  stoweidlem17  41712  stoweidlem21  41716  stoweidlem43  41738  stoweidlem51  41746  wallispi  41765