Theorem vtoclga 3522

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1548   ∈ wcel 2121

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-tru 1551  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816

This theorem is referenced by:  vtocl2ga  3523  vtocl3ga  3526  vtoclri  3530  disjxiun  5072  wfis3  6312  opabiota  6913  fvmpt3  6944  fvmptss  6952  fnressn  7105  fressnfv  7107  caovord  7571  caovmo  7597  ordunisuc  7776  tfis3  7802  fpr2a  8246  frrdmcl  8252  onfununi  8275  smogt  8301  tz7.44-1  8339  tz7.44-2  8340  tz7.44-3  8341  nnacl  8541  nnmcl  8542  nnecl  8543  nnacom  8547  nnaass  8552  nndi  8553  nnmass  8554  nnmsucr  8555  nnmcom  8556  nnmordi  8561  ixpfn  8845  findcard  9092  findcard2  9093  marypha1  9341  cantnfle  9587  cantnflem1  9605  cnfcom  9616  frr2  9679  fseqenlem1  9941  nnadju  10115  ackbij1lem8  10143  cardcf  10169  cfsmolem  10187  wunex2  10656  ingru  10733  recrecnq  10885  prlem934  10951  nn1suc  12191  uzind4s2  12854  rpnnen1lem6  12927  cnref1o  12930  xmulasslem  13232  om2uzsuci  13905  expcl2lem  14030  hashpw  14393  seqcoll  14421  climub  15619  climserle  15620  sumrblem  15668  fsumcvg  15669  summolem2a  15672  infcvgaux2i  15818  prodfn0  15854  prodfrec  15855  prodrblem  15889  fprodcvg  15890  prodmolem2a  15894  divalglem8  16364  bezoutlem1  16503  alginv  16539  algcvg  16540  algcvga  16543  algfx  16544  prmind2  16649  prmpwdvds  16870  cnextfvval  24052  xrsxmet  24797  xrhmeo  24935  cmetcaulem  25277  bcth3  25320  itg2addlem  25747  taylfval  26346  sinord  26520  logexprlim  27210  lgsdir2lem4  27313  noseqind  28306  hlim2  31285  elnlfn  32021  lnconi  32126  chirredlem3  32485  chirredlem4  32486  cnre2csqlem  34106  eulerpartlemsf  34555  eulerpartlemn  34577  bnj1321  35224  bnj1418  35237  subfacp1lem1  35422  nn0prpwlem  36565  findreccl  36696  weiunlem  36706  mptsnunlem  37715  rdgeqoa  37747  domalom  37781  poimirlem22  38024  poimirlem26  38028  mblfinlem3  38041  mblfinlem4  38042  ismblfin  38043  ftc1anclem3  38077  ftc1anclem8  38082  sdclem2  38124  iscringd  38380  renegclALT  39470  zindbi  43406  fmuldfeq  46042  sumnnodd  46089  iblspltprt  46430  stoweidlem2  46459  stoweidlem17  46474  stoweidlem21  46478  stoweidlem43  46500  stoweidlem51  46508  wallispi  46527