Theorem vtoclga 3521

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ∈ wcel 2114

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812

This theorem is referenced by:  vtocl2ga  3522  vtocl3ga  3527  vtoclri  3533  disjxiun  5083  wfis3  6317  opabiota  6918  fvmpt3  6948  fvmptss  6956  fnressn  7107  fressnfv  7109  caovord  7573  caovmo  7599  ordunisuc  7778  tfis3  7804  fpr2a  8247  frrdmcl  8253  onfununi  8276  smogt  8302  tz7.44-1  8340  tz7.44-2  8341  tz7.44-3  8342  nnacl  8542  nnmcl  8543  nnecl  8544  nnacom  8548  nnaass  8553  nndi  8554  nnmass  8555  nnmsucr  8556  nnmcom  8557  nnmordi  8562  ixpfn  8846  findcard  9093  findcard2  9094  marypha1  9342  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  24044  xrsxmet  24789  xrhmeo  24927  cmetcaulem  25269  bcth3  25312  itg2addlem  25739  taylfval  26339  sinord  26515  logexprlim  27206  lgsdir2lem4  27309  noseqind  28302  hlim2  31282  elnlfn  32018  lnconi  32123  chirredlem3  32482  chirredlem4  32483  cnre2csqlem  34074  eulerpartlemsf  34523  eulerpartlemn  34545  bnj1321  35189  bnj1418  35202  subfacp1lem1  35381  nn0prpwlem  36524  findreccl  36655  weiunlem  36665  mptsnunlem  37674  rdgeqoa  37706  domalom  37740  poimirlem22  37983  poimirlem26  37987  mblfinlem3  38000  mblfinlem4  38001  ismblfin  38002  ftc1anclem3  38036  ftc1anclem8  38041  sdclem2  38083  iscringd  38339  renegclALT  39429  zindbi  43398  fmuldfeq  46037  sumnnodd  46084  iblspltprt  46425  stoweidlem2  46454  stoweidlem17  46469  stoweidlem21  46473  stoweidlem43  46495  stoweidlem51  46503  wallispi  46522