Theorem vtoclga 3503

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817

This theorem is referenced by:  vtocl2ga  3504  vtoclri  3515  disjxiun  5067  wfis3  6249  opabiota  6833  fvmpt3  6861  fvmptss  6869  fnressn  7012  fressnfv  7014  caovord  7461  caovmo  7487  ordunisuc  7654  tfis3  7679  fpr2a  8089  frrdmcl  8095  wfr2aOLD  8128  onfununi  8143  smogt  8169  tz7.44-1  8208  tz7.44-2  8209  tz7.44-3  8210  nnacl  8404  nnmcl  8405  nnecl  8406  nnacom  8410  nnaass  8415  nndi  8416  nnmass  8417  nnmsucr  8418  nnmcom  8419  nnmordi  8424  ixpfn  8649  findcard  8908  findcard2  8909  findcard2OLD  8986  marypha1  9123  cantnfle  9359  cantnflem1  9377  cnfcom  9388  frr2  9449  fseqenlem1  9711  nnadju  9884  ackbij1lem8  9914  cardcf  9939  cfsmolem  9957  wunex2  10425  ingru  10502  recrecnq  10654  prlem934  10720  nn1suc  11925  uzind4s2  12578  rpnnen1lem6  12651  cnref1o  12654  xmulasslem  12948  om2uzsuci  13596  expcl2lem  13722  hashpw  14079  seqcoll  14106  climub  15301  climserle  15302  sumrblem  15351  fsumcvg  15352  summolem2a  15355  infcvgaux2i  15498  prodfn0  15534  prodfrec  15535  prodrblem  15567  fprodcvg  15568  prodmolem2a  15572  divalglem8  16037  bezoutlem1  16175  alginv  16208  algcvg  16209  algcvga  16212  algfx  16213  prmind2  16318  prmpwdvds  16533  cnextfvval  23124  xrsxmet  23878  xrhmeo  24015  cmetcaulem  24357  bcth3  24400  itg2addlem  24828  taylfval  25423  sinord  25595  logexprlim  26278  lgsdir2lem4  26381  hlim2  29455  elnlfn  30191  lnconi  30296  chirredlem3  30655  chirredlem4  30656  cnre2csqlem  31762  eulerpartlemsf  32226  eulerpartlemn  32248  bnj1321  32907  bnj1418  32920  subfacp1lem1  33041  nn0prpwlem  34438  findreccl  34569  mptsnunlem  35436  rdgeqoa  35468  domalom  35502  poimirlem22  35726  poimirlem26  35730  mblfinlem3  35743  mblfinlem4  35744  ismblfin  35745  ftc1anclem3  35779  ftc1anclem8  35784  sdclem2  35827  iscringd  36083  renegclALT  36904  zindbi  40684  fmuldfeq  43014  sumnnodd  43061  iblspltprt  43404  stoweidlem2  43433  stoweidlem17  43448  stoweidlem21  43452  stoweidlem43  43474  stoweidlem51  43482  wallispi  43501