Theorem vtoclga 2881

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1398   ∈ wcel 2203

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-v 2815

This theorem is referenced by:  vtoclri  2892  ssuni  3936  ordtriexmid  4643  onsucsssucexmid  4649  tfis3  4708  fvmpt3  5756  fvmptssdm  5762  fnressn  5870  fressnfv  5871  caovord  6226  caovimo  6248  tfrlem1  6539  nnacl  6713  nnmcl  6714  nnacom  6717  nnaass  6718  nndi  6719  nnmass  6720  nnmsucr  6721  nnmcom  6722  nnsucsssuc  6725  nntri3or  6726  nnaordi  6741  nnaword  6744  nnmordi  6749  nnaordex  6761  ixpfn  6939  findcard  7145  findcard2  7146  findcard2s  7147  exmidomni  7433  indpi  7657  prarloclem3  7812  uzind4s2  9923  cnref1o  9983  frec2uzrdg  10771  expcl2lemap  10913  seq3coll  11214  climub  12029  climserle  12030  fsum3cvg  12064  summodclem2a  12067  prodfap0  12231  prodfrecap  12232  fproddccvg  12258  alginv  12744  algcvg  12745  algcvga  12748  algfx  12749  prmind2  12817  prmpwdvds  13053  lgsdir2lem4  15904