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  4570  onsucsssucexmid  4576  tfis3  4635  fvmpt3  5660  fvmptssdm  5666  fnressn  5772  fressnfv  5773  caovord  6120  caovimo  6142  tfrlem1  6396  nnacl  6568  nnmcl  6569  nnacom  6572  nnaass  6573  nndi  6574  nnmass  6575  nnmsucr  6576  nnmcom  6577  nnsucsssuc  6580  nntri3or  6581  nnaordi  6596  nnaword  6599  nnmordi  6604  nnaordex  6616  ixpfn  6793  findcard  6987  findcard2  6988  findcard2s  6989  exmidomni  7246  indpi  7457  prarloclem3  7612  uzind4s2  9714  cnref1o  9774  frec2uzrdg  10556  expcl2lemap  10698  seq3coll  10989  climub  11688  climserle  11689  fsum3cvg  11722  summodclem2a  11725  prodfap0  11889  prodfrecap  11890  fproddccvg  11916  alginv  12402  algcvg  12403  algcvga  12406  algfx  12407  prmind2  12475  prmpwdvds  12711  lgsdir2lem4  15541