Theorem vtoclga 3532

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2109

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803

This theorem is referenced by:  vtocl2ga  3533  vtocl3ga  3538  vtoclri  3545  disjxiun  5089  wfis3  6305  opabiota  6905  fvmpt3  6934  fvmptss  6942  fnressn  7092  fressnfv  7094  caovord  7560  caovmo  7586  ordunisuc  7765  tfis3  7791  fpr2a  8235  frrdmcl  8241  onfununi  8264  smogt  8290  tz7.44-1  8328  tz7.44-2  8329  tz7.44-3  8330  nnacl  8529  nnmcl  8530  nnecl  8531  nnacom  8535  nnaass  8540  nndi  8541  nnmass  8542  nnmsucr  8543  nnmcom  8544  nnmordi  8549  ixpfn  8830  findcard  9077  findcard2  9078  marypha1  9324  cantnfle  9567  cantnflem1  9585  cnfcom  9596  frr2  9656  fseqenlem1  9918  nnadju  10092  ackbij1lem8  10120  cardcf  10146  cfsmolem  10164  wunex2  10632  ingru  10709  recrecnq  10861  prlem934  10927  nn1suc  12150  uzind4s2  12810  rpnnen1lem6  12883  cnref1o  12886  xmulasslem  13187  om2uzsuci  13855  expcl2lem  13980  hashpw  14343  seqcoll  14371  climub  15569  climserle  15570  sumrblem  15618  fsumcvg  15619  summolem2a  15622  infcvgaux2i  15765  prodfn0  15801  prodfrec  15802  prodrblem  15836  fprodcvg  15837  prodmolem2a  15841  divalglem8  16311  bezoutlem1  16450  alginv  16486  algcvg  16487  algcvga  16490  algfx  16491  prmind2  16596  prmpwdvds  16816  cnextfvval  23950  xrsxmet  24696  xrhmeo  24842  cmetcaulem  25186  bcth3  25229  itg2addlem  25657  taylfval  26264  sinord  26441  logexprlim  27134  lgsdir2lem4  27237  noseqind  28193  hlim2  31140  elnlfn  31876  lnconi  31981  chirredlem3  32340  chirredlem4  32341  cnre2csqlem  33893  eulerpartlemsf  34343  eulerpartlemn  34365  bnj1321  35010  bnj1418  35023  subfacp1lem1  35172  nn0prpwlem  36316  findreccl  36447  weiunlem2  36457  mptsnunlem  37332  rdgeqoa  37364  domalom  37398  poimirlem22  37642  poimirlem26  37646  mblfinlem3  37659  mblfinlem4  37660  ismblfin  37661  ftc1anclem3  37695  ftc1anclem8  37700  sdclem2  37742  iscringd  37998  renegclALT  38962  zindbi  42939  fmuldfeq  45584  sumnnodd  45631  iblspltprt  45974  stoweidlem2  46003  stoweidlem17  46018  stoweidlem21  46022  stoweidlem43  46044  stoweidlem51  46052  wallispi  46071  upwordisword  46882