Theorem vtoclga 3532

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1541   ∈ wcel 2106

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2708

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2715  df-cleq 2729  df-clel 2815

This theorem is referenced by:  vtocl2ga  3533  vtoclri  3543  disjxiun  5100  wfis3  6313  opabiota  6921  fvmpt3  6949  fvmptss  6957  fnressn  7100  fressnfv  7102  caovord  7559  caovmo  7585  ordunisuc  7759  tfis3  7786  fpr2a  8225  frrdmcl  8231  wfr2aOLD  8264  onfununi  8279  smogt  8305  tz7.44-1  8344  tz7.44-2  8345  tz7.44-3  8346  nnacl  8550  nnmcl  8551  nnecl  8552  nnacom  8556  nnaass  8561  nndi  8562  nnmass  8563  nnmsucr  8564  nnmcom  8565  nnmordi  8570  ixpfn  8799  findcard  9065  findcard2  9066  findcard2OLD  9186  marypha1  9328  cantnfle  9565  cantnflem1  9583  cnfcom  9594  frr2  9654  fseqenlem1  9918  nnadju  10091  ackbij1lem8  10121  cardcf  10146  cfsmolem  10164  wunex2  10632  ingru  10709  recrecnq  10861  prlem934  10927  nn1suc  12133  uzind4s2  12788  rpnnen1lem6  12861  cnref1o  12864  xmulasslem  13158  om2uzsuci  13807  expcl2lem  13933  hashpw  14289  seqcoll  14316  climub  15505  climserle  15506  sumrblem  15555  fsumcvg  15556  summolem2a  15559  infcvgaux2i  15702  prodfn0  15738  prodfrec  15739  prodrblem  15771  fprodcvg  15772  prodmolem2a  15776  divalglem8  16241  bezoutlem1  16379  alginv  16410  algcvg  16411  algcvga  16414  algfx  16415  prmind2  16520  prmpwdvds  16735  cnextfvval  23367  xrsxmet  24123  xrhmeo  24260  cmetcaulem  24603  bcth3  24646  itg2addlem  25074  taylfval  25669  sinord  25841  logexprlim  26524  lgsdir2lem4  26627  hlim2  29962  elnlfn  30698  lnconi  30803  chirredlem3  31162  chirredlem4  31163  cnre2csqlem  32294  eulerpartlemsf  32762  eulerpartlemn  32784  bnj1321  33442  bnj1418  33455  subfacp1lem1  33576  nn0prpwlem  34725  findreccl  34856  mptsnunlem  35740  rdgeqoa  35772  domalom  35806  poimirlem22  36031  poimirlem26  36035  mblfinlem3  36048  mblfinlem4  36049  ismblfin  36050  ftc1anclem3  36084  ftc1anclem8  36089  sdclem2  36132  iscringd  36388  renegclALT  37356  zindbi  41172  fmuldfeq  43718  sumnnodd  43765  iblspltprt  44108  stoweidlem2  44137  stoweidlem17  44152  stoweidlem21  44156  stoweidlem43  44178  stoweidlem51  44186  wallispi  44205  upwordisword  45014