Theorem vtoclga 3576

Description: Implicit substitution of a class for a setvar variable. (Contributed by NM, 20-Aug-1995.) Avoid ax-10 2145 and ax-11 2161. (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 2902	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
2		vtoclga.1	. . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
3	1, 2	imbi12d 347	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 → 𝜑) ↔ (𝐴 ∈ 𝐵 → 𝜓)))
4		vtoclga.2	. . 3 ⊢ (𝑥 ∈ 𝐵 → 𝜑)
5	3, 4	vtoclg 3569	. 2 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ 𝐵 → 𝜓))
6	5	pm2.43i 52	1 ⊢ (𝐴 ∈ 𝐵 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1537   ∈ wcel 2114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2816  df-clel 2895

This theorem is referenced by:  vtocl2ga  3577  vtoclri  3587  disjxiun  5065  wfis3  6191  opabiota  6748  fvmpt3  6774  fvmptss  6782  fnressn  6922  fressnfv  6924  caovord  7361  caovmo  7387  ordunisuc  7549  tfis3  7574  wfr2a  7974  onfununi  7980  smogt  8006  tz7.44-1  8044  tz7.44-2  8045  tz7.44-3  8046  nnacl  8239  nnmcl  8240  nnecl  8241  nnacom  8245  nnaass  8250  nndi  8251  nnmass  8252  nnmsucr  8253  nnmcom  8254  nnmordi  8259  ixpfn  8469  findcard  8759  findcard2  8760  marypha1  8900  cantnfle  9136  cantnflem1  9154  cnfcom  9165  fseqenlem1  9452  ackbij1lem8  9651  cardcf  9676  cfsmolem  9694  wunex2  10162  ingru  10239  recrecnq  10391  prlem934  10457  nn1suc  11662  uzind4s2  12312  rpnnen1lem6  12384  cnref1o  12387  xmulasslem  12681  om2uzsuci  13319  expcl2lem  13444  hashpw  13800  seqcoll  13825  climub  15020  climserle  15021  sumrblem  15070  fsumcvg  15071  summolem2a  15074  infcvgaux2i  15215  prodfn0  15252  prodfrec  15253  prodrblem  15285  fprodcvg  15286  prodmolem2a  15290  divalglem8  15753  bezoutlem1  15889  alginv  15921  algcvg  15922  algcvga  15925  algfx  15926  prmind2  16031  prmpwdvds  16242  cnextfvval  22675  xrsxmet  23419  xrhmeo  23552  cmetcaulem  23893  bcth3  23936  itg2addlem  24361  taylfval  24949  sinord  25120  logexprlim  25803  lgsdir2lem4  25906  hlim2  28971  elnlfn  29707  lnconi  29812  chirredlem3  30171  chirredlem4  30172  cnre2csqlem  31155  eulerpartlemsf  31619  eulerpartlemn  31641  bnj1321  32301  bnj1418  32314  subfacp1lem1  32428  frins3  33095  fpr2  33142  frr2  33147  nn0prpwlem  33672  findreccl  33803  mptsnunlem  34621  rdgeqoa  34653  domalom  34687  poimirlem22  34916  poimirlem26  34920  mblfinlem3  34933  mblfinlem4  34934  ismblfin  34935  ftc1anclem3  34971  ftc1anclem8  34976  sdclem2  35019  iscringd  35278  renegclALT  36101  zindbi  39550  fmuldfeq  41871  sumnnodd  41918  iblspltprt  42265  stoweidlem2  42294  stoweidlem17  42309  stoweidlem21  42313  stoweidlem43  42335  stoweidlem51  42343  wallispi  42362