Theorem vtoclga 3540

Description: Implicit substitution of a class for a setvar variable. (Contributed by NM, 20-Aug-1995.) Avoid ax-10 2175 and ax-11 2191. (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 3521	. 2 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ 𝐵 → 𝜓))
6	5	pm2.43i 53	1 ⊢ (𝐴 ∈ 𝐵 → 𝜓)

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-tru 1572  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837

This theorem is used by:  vtocl2ga  3541  vtocl3ga  3544  vtoclri  3548  disjxiun  5105  wfis3  6358  opabiota  6963  fvmpt3  6994  fvmptss  7002  fnressn  7155  fressnfv  7157  caovord  7623  caovmo  7649  ordunisuc  7826  tfis3  7852  fpr2a  8297  frrdmcl  8303  onfununi  8326  smogt  8352  tz7.44-1  8391  tz7.44-2  8392  tz7.44-3  8393  nnacl  8595  nnmcl  8596  nnecl  8597  nnacom  8601  nnaass  8606  nndi  8607  nnmass  8608  nnmsucr  8609  nnmcom  8610  nnmordi  8615  ixpfn  8899  findcard  9146  findcard2  9147  marypha1  9392  cantnfle  9638  cantnflem1  9656  cnfcom  9667  frr2  9730  fseqenlem1  10015  nnadju  10188  ackbij1lem8  10216  cardcf  10241  cfsmolem  10260  wunex2  10729  ingru  10806  recrecnq  10958  prlem934  11024  nn1suc  12261  uzind4s2  12939  rpnnen1lem6  13012  cnref1o  13015  xmulasslem  13317  om2uzsuci  13991  expcl2lem  14116  hashpw  14480  seqcoll  14508  climub  15720  climserle  15721  sumrblem  15769  fsumcvg  15770  summolem2a  15773  infcvgaux2i  15919  prodfn0  15955  prodfrec  15956  prodrblem  15990  fprodcvg  15991  prodmolem2a  15995  divalglem8  16464  bezoutlem1  16603  alginv  16639  algcvg  16640  algcvga  16643  algfx  16644  prmind2  16749  prmpwdvds  16970  cnextfvval  24233  xrsxmet  24978  xrhmeo  25116  cmetcaulem  25458  bcth3  25501  itg2addlem  25928  taylfval  26533  sinord  26710  logexprlim  27400  lgsdir2lem4  27503  noseqind  28496  hlim2  31555  elnlfn  32291  lnconi  32396  chirredlem3  32755  chirredlem4  32756  cnre2csqlem  34309  eulerpartlemsf  34758  eulerpartlemn  34780  bnj1321  35424  bnj1418  35437  subfacp1lem1  35679  nn0prpwlem  36861  findreccl  36992  weiunlem  37002  mptsnunlem  38012  rdgeqoa  38044  domalom  38078  poimirlem22  38321  poimirlem26  38325  mblfinlem3  38338  mblfinlem4  38339  ismblfin  38340  ftc1anclem3  38374  ftc1anclem8  38379  sdclem2  38421  iscringd  38677  renegclALT  39765  zindbi  43701  fmuldfeq  46327  sumnnodd  46374  iblspltprt  46715  stoweidlem2  46744  stoweidlem17  46759  stoweidlem21  46763  stoweidlem43  46785  stoweidlem51  46793  wallispi  46812