Theorem vtoclga 2815

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1363   ∈ wcel 2158

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 710  ax-5 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-ext 2169

This theorem depends on definitions:  df-bi 117  df-tru 1366  df-nf 1471  df-sb 1773  df-clab 2174  df-cleq 2180  df-clel 2183  df-nfc 2318  df-v 2751

This theorem is referenced by:  vtoclri  2824  ssuni  3843  ordtriexmid  4532  onsucsssucexmid  4538  tfis3  4597  fvmpt3  5608  fvmptssdm  5613  fnressn  5715  fressnfv  5716  caovord  6060  caovimo  6082  tfrlem1  6323  nnacl  6495  nnmcl  6496  nnacom  6499  nnaass  6500  nndi  6501  nnmass  6502  nnmsucr  6503  nnmcom  6504  nnsucsssuc  6507  nntri3or  6508  nnaordi  6523  nnaword  6526  nnmordi  6531  nnaordex  6543  ixpfn  6718  findcard  6902  findcard2  6903  findcard2s  6904  exmidomni  7154  indpi  7355  prarloclem3  7510  uzind4s2  9605  cnref1o  9664  frec2uzrdg  10423  expcl2lemap  10546  seq3coll  10836  climub  11366  climserle  11367  fsum3cvg  11400  summodclem2a  11403  prodfap0  11567  prodfrecap  11568  fproddccvg  11594  alginv  12061  algcvg  12062  algcvga  12065  algfx  12066  prmind2  12134  prmpwdvds  12367  lgsdir2lem4  14785