Theorem vtoclga 2839

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1373   ∈ wcel 2176

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-v 2774

This theorem is referenced by:  vtoclri  2848  ssuni  3872  ordtriexmid  4569  onsucsssucexmid  4575  tfis3  4634  fvmpt3  5658  fvmptssdm  5664  fnressn  5770  fressnfv  5771  caovord  6118  caovimo  6140  tfrlem1  6394  nnacl  6566  nnmcl  6567  nnacom  6570  nnaass  6571  nndi  6572  nnmass  6573  nnmsucr  6574  nnmcom  6575  nnsucsssuc  6578  nntri3or  6579  nnaordi  6594  nnaword  6597  nnmordi  6602  nnaordex  6614  ixpfn  6791  findcard  6985  findcard2  6986  findcard2s  6987  exmidomni  7244  indpi  7455  prarloclem3  7610  uzind4s2  9712  cnref1o  9772  frec2uzrdg  10554  expcl2lemap  10696  seq3coll  10987  climub  11655  climserle  11656  fsum3cvg  11689  summodclem2a  11692  prodfap0  11856  prodfrecap  11857  fproddccvg  11883  alginv  12369  algcvg  12370  algcvga  12373  algfx  12374  prmind2  12442  prmpwdvds  12678  lgsdir2lem4  15508