Theorem vtoclga 3577

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537   ∈ wcel 2106

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814

This theorem is referenced by:  vtocl2ga  3578  vtocl3ga  3583  vtoclri  3590  disjxiun  5145  wfis3  6384  opabiota  6991  fvmpt3  7020  fvmptss  7028  fnressn  7178  fressnfv  7180  caovord  7644  caovmo  7670  ordunisuc  7852  tfis3  7879  fpr2a  8326  frrdmcl  8332  wfr2aOLD  8365  onfununi  8380  smogt  8406  tz7.44-1  8445  tz7.44-2  8446  tz7.44-3  8447  nnacl  8648  nnmcl  8649  nnecl  8650  nnacom  8654  nnaass  8659  nndi  8660  nnmass  8661  nnmsucr  8662  nnmcom  8663  nnmordi  8668  ixpfn  8942  findcard  9202  findcard2  9203  marypha1  9472  cantnfle  9709  cantnflem1  9727  cnfcom  9738  frr2  9798  fseqenlem1  10062  nnadju  10236  ackbij1lem8  10264  cardcf  10290  cfsmolem  10308  wunex2  10776  ingru  10853  recrecnq  11005  prlem934  11071  nn1suc  12286  uzind4s2  12949  rpnnen1lem6  13022  cnref1o  13025  xmulasslem  13324  om2uzsuci  13986  expcl2lem  14111  hashpw  14472  seqcoll  14500  climub  15695  climserle  15696  sumrblem  15744  fsumcvg  15745  summolem2a  15748  infcvgaux2i  15891  prodfn0  15927  prodfrec  15928  prodrblem  15962  fprodcvg  15963  prodmolem2a  15967  divalglem8  16434  bezoutlem1  16573  alginv  16609  algcvg  16610  algcvga  16613  algfx  16614  prmind2  16719  prmpwdvds  16938  cnextfvval  24089  xrsxmet  24845  xrhmeo  24991  cmetcaulem  25336  bcth3  25379  itg2addlem  25808  taylfval  26415  sinord  26591  logexprlim  27284  lgsdir2lem4  27387  noseqind  28313  hlim2  31221  elnlfn  31957  lnconi  32062  chirredlem3  32421  chirredlem4  32422  cnre2csqlem  33871  eulerpartlemsf  34341  eulerpartlemn  34363  bnj1321  35020  bnj1418  35033  subfacp1lem1  35164  nn0prpwlem  36305  findreccl  36436  weiunlem2  36446  mptsnunlem  37321  rdgeqoa  37353  domalom  37387  poimirlem22  37629  poimirlem26  37633  mblfinlem3  37646  mblfinlem4  37647  ismblfin  37648  ftc1anclem3  37682  ftc1anclem8  37687  sdclem2  37729  iscringd  37985  renegclALT  38945  zindbi  42935  fmuldfeq  45539  sumnnodd  45586  iblspltprt  45929  stoweidlem2  45958  stoweidlem17  45973  stoweidlem21  45977  stoweidlem43  45999  stoweidlem51  46007  wallispi  46026  upwordisword  46835