Theorem vtoclga 3513

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539   ∈ wcel 2106

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816

This theorem is referenced by:  vtocl2ga  3514  vtoclri  3525  disjxiun  5071  wfis3  6264  opabiota  6851  fvmpt3  6879  fvmptss  6887  fnressn  7030  fressnfv  7032  caovord  7483  caovmo  7509  ordunisuc  7679  tfis3  7704  fpr2a  8118  frrdmcl  8124  wfr2aOLD  8157  onfununi  8172  smogt  8198  tz7.44-1  8237  tz7.44-2  8238  tz7.44-3  8239  nnacl  8442  nnmcl  8443  nnecl  8444  nnacom  8448  nnaass  8453  nndi  8454  nnmass  8455  nnmsucr  8456  nnmcom  8457  nnmordi  8462  ixpfn  8691  findcard  8946  findcard2  8947  findcard2OLD  9056  marypha1  9193  cantnfle  9429  cantnflem1  9447  cnfcom  9458  frr2  9518  fseqenlem1  9780  nnadju  9953  ackbij1lem8  9983  cardcf  10008  cfsmolem  10026  wunex2  10494  ingru  10571  recrecnq  10723  prlem934  10789  nn1suc  11995  uzind4s2  12649  rpnnen1lem6  12722  cnref1o  12725  xmulasslem  13019  om2uzsuci  13668  expcl2lem  13794  hashpw  14151  seqcoll  14178  climub  15373  climserle  15374  sumrblem  15423  fsumcvg  15424  summolem2a  15427  infcvgaux2i  15570  prodfn0  15606  prodfrec  15607  prodrblem  15639  fprodcvg  15640  prodmolem2a  15644  divalglem8  16109  bezoutlem1  16247  alginv  16280  algcvg  16281  algcvga  16284  algfx  16285  prmind2  16390  prmpwdvds  16605  cnextfvval  23216  xrsxmet  23972  xrhmeo  24109  cmetcaulem  24452  bcth3  24495  itg2addlem  24923  taylfval  25518  sinord  25690  logexprlim  26373  lgsdir2lem4  26476  hlim2  29554  elnlfn  30290  lnconi  30395  chirredlem3  30754  chirredlem4  30755  cnre2csqlem  31860  eulerpartlemsf  32326  eulerpartlemn  32348  bnj1321  33007  bnj1418  33020  subfacp1lem1  33141  nn0prpwlem  34511  findreccl  34642  mptsnunlem  35509  rdgeqoa  35541  domalom  35575  poimirlem22  35799  poimirlem26  35803  mblfinlem3  35816  mblfinlem4  35817  ismblfin  35818  ftc1anclem3  35852  ftc1anclem8  35857  sdclem2  35900  iscringd  36156  renegclALT  36977  zindbi  40768  fmuldfeq  43124  sumnnodd  43171  iblspltprt  43514  stoweidlem2  43543  stoweidlem17  43558  stoweidlem21  43562  stoweidlem43  43584  stoweidlem51  43592  wallispi  43611  upwordisword  46516