Theorem vtoclga 2870

Description: Implicit substitution of a class for a setvar variable. (Contributed by NM, 20-Aug-1995.)

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		nfcv 2374	. 2 ⊢ Ⅎ𝑥𝐴
2		nfv 1576	. 2 ⊢ Ⅎ𝑥𝜓
3		vtoclga.1	. 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
4		vtoclga.2	. 2 ⊢ (𝑥 ∈ 𝐵 → 𝜑)
5	1, 2, 3, 4	vtoclgaf 2869	1 ⊢ (𝐴 ∈ 𝐵 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1397   ∈ wcel 2202

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-v 2804

This theorem is referenced by:  vtoclri  2881  ssuni  3915  ordtriexmid  4619  onsucsssucexmid  4625  tfis3  4684  fvmpt3  5725  fvmptssdm  5731  fnressn  5839  fressnfv  5840  caovord  6193  caovimo  6215  tfrlem1  6473  nnacl  6647  nnmcl  6648  nnacom  6651  nnaass  6652  nndi  6653  nnmass  6654  nnmsucr  6655  nnmcom  6656  nnsucsssuc  6659  nntri3or  6660  nnaordi  6675  nnaword  6678  nnmordi  6683  nnaordex  6695  ixpfn  6872  findcard  7076  findcard2  7077  findcard2s  7078  exmidomni  7340  indpi  7561  prarloclem3  7716  uzind4s2  9824  cnref1o  9884  frec2uzrdg  10670  expcl2lemap  10812  seq3coll  11105  climub  11904  climserle  11905  fsum3cvg  11938  summodclem2a  11941  prodfap0  12105  prodfrecap  12106  fproddccvg  12132  alginv  12618  algcvg  12619  algcvga  12622  algfx  12623  prmind2  12691  prmpwdvds  12927  lgsdir2lem4  15759