Theorem vtoclga 3539

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2145

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837

This theorem is used by:  vtocl2ga  3540  vtocl3ga  3543  vtoclri  3547  disjxiun  5104  wfis3  6359  opabiota  6964  fvmpt3  6995  fvmptss  7003  fnressn  7158  fressnfv  7160  caovord  7628  caovmo  7654  ordunisuc  7831  tfis3  7857  fpr2a  8304  frrdmcl  8310  onfununi  8333  smogt  8359  tz7.44-1  8398  tz7.44-2  8399  tz7.44-3  8400  nnacl  8602  nnmcl  8603  nnecl  8604  nnacom  8608  nnaass  8613  nndi  8614  nnmass  8615  nnmsucr  8616  nnmcom  8617  nnmordi  8622  ixpfn  8913  findcard  9161  findcard2  9162  marypha1  9407  cantnfle  9653  cantnflem1  9671  cnfcom  9682  frr2  9745  fseqenlem1  10030  nnadju  10203  ackbij1lem8  10231  cardcf  10256  cfsmolem  10275  wunex2  10750  ingru  10827  recrecnq  10979  prlem934  11045  nn1suc  12282  uzind4s2  12961  rpnnen1lem6  13034  cnref1o  13037  xmulasslem  13339  om2uzsuci  14014  expcl2lem  14139  hashpw  14503  seqcoll  14531  climub  15751  climserle  15752  sumrblem  15799  fsumcvg  15800  summolem2a  15803  infcvgaux2i  15949  prodfn0  15985  prodfrec  15986  prodrblem  16020  fprodcvg  16021  prodmolem2a  16025  divalglem8  16494  bezoutlem1  16633  alginv  16669  algcvg  16670  algcvga  16673  algfx  16674  prmind2  16779  prmpwdvds  17000  cnextfvval  24292  xrsxmet  25037  xrhmeo  25175  cmetcaulem  25517  bcth3  25560  itg2addlem  25987  taylfval  26592  sinord  26769  logexprlim  27459  lgsdir2lem4  27562  noseqind  28555  hlim2  31659  elnlfn  32395  lnconi  32500  chirredlem3  32859  chirredlem4  32860  cnre2csqlem  34407  eulerpartlemsf  34857  eulerpartlemn  34879  bnj1321  35523  bnj1418  35536  subfacp1lem1  35745  nn0prpwlem  36928  findreccl  37059  weiunlem  37069  mptsnunlem  38079  rdgeqoa  38111  domalom  38145  poimirlem22  38378  poimirlem26  38382  mblfinlem3  38395  mblfinlem4  38396  ismblfin  38397  ftc1anclem3  38431  ftc1anclem8  38436  sdclem2  38479  iscringd  38735  renegclALT  39823  zindbi  43774  fmuldfeq  46400  sumnnodd  46447  iblspltprt  46788  stoweidlem2  46817  stoweidlem17  46832  stoweidlem21  46836  stoweidlem43  46858  stoweidlem51  46866  wallispi  46885