Theorem vtoclga 3536

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 2848	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
2		vtoclga.1	. . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
3	1, 2	imbi12d 347	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 → 𝜑) ↔ (𝐴 ∈ 𝐵 → 𝜓)))
4		vtoclga.2	. . 3 ⊢ (𝑥 ∈ 𝐵 → 𝜑)
5	3, 4	vtoclg 3517	. 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 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835

This theorem is used by:  vtocl2ga  3537  vtocl3ga  3540  vtoclri  3544  disjxiun  5100  wfis3  6350  opabiota  6956  fvmpt3  6987  fvmptss  6995  fnressn  7151  fressnfv  7153  caovord  7621  caovmo  7647  ordunisuc  7827  tfis3  7853  fpr2a  8299  frrdmcl  8305  onfununi  8328  smogt  8354  tz7.44-1  8393  tz7.44-2  8394  tz7.44-3  8395  nnacl  8599  nnmcl  8600  nnecl  8601  nnacom  8605  nnaass  8610  nndi  8611  nnmass  8612  nnmsucr  8613  nnmcom  8614  nnmordi  8619  ixpfn  8910  findcard  9158  findcard2  9159  marypha1  9404  cantnfle  9650  cantnflem1  9668  cnfcom  9679  frr2  9742  fseqenlem1  10060  nnadju  10233  ackbij1lem8  10261  cardcf  10286  cfsmolem  10305  wunex2  10780  ingru  10857  recrecnq  11009  prlem934  11075  nn1suc  12312  uzind4s2  12991  rpnnen1lem6  13065  cnref1o  13068  xmulasslem  13370  om2uzsuci  14045  expcl2lem  14170  hashpw  14534  seqcoll  14562  climub  15782  climserle  15783  sumrblem  15830  fsumcvg  15831  summolem2a  15834  infcvgaux2i  15980  prodfn0  16016  prodfrec  16017  prodrblem  16049  fprodcvg  16050  prodmolem2a  16054  divalglem8  16523  bezoutlem1  16662  alginv  16698  algcvg  16699  algcvga  16702  algfx  16703  prmind2  16808  prmpwdvds  17029  cnextfvval  24331  xrsxmet  25076  xrhmeo  25214  cmetcaulem  25556  bcth3  25599  itg2addlem  26026  taylfval  26635  sinord  26811  logexprlim  27501  lgsdir2lem4  27604  noseqind  28597  hlim2  31713  elnlfn  32449  lnconi  32554  chirredlem3  32913  chirredlem4  32914  cnre2csqlem  34461  eulerpartlemsf  34911  eulerpartlemn  34933  bnj1321  35577  bnj1418  35590  subfacp1lem1  35859  nn0prpwlem  37026  findreccl  37157  weiunlem  37167  mptsnunlem  38175  rdgeqoa  38207  domalom  38241  poimirlem22  38474  poimirlem26  38478  mblfinlem3  38491  mblfinlem4  38492  ismblfin  38493  ftc1anclem3  38527  ftc1anclem8  38532  sdclem2  38590  iscringd  38846  renegclALT  39934  zindbi  43885  fmuldfeq  46511  sumnnodd  46558  iblspltprt  46899  stoweidlem2  46928  stoweidlem17  46943  stoweidlem21  46947  stoweidlem43  46969  stoweidlem51  46977  wallispi  46996