Theorem vtoclga 2803

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1353   ∈ wcel 2148

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2739

This theorem is referenced by:  vtoclri  2812  ssuni  3831  ordtriexmid  4520  onsucsssucexmid  4526  tfis3  4585  fvmpt3  5595  fvmptssdm  5600  fnressn  5702  fressnfv  5703  caovord  6045  caovimo  6067  tfrlem1  6308  nnacl  6480  nnmcl  6481  nnacom  6484  nnaass  6485  nndi  6486  nnmass  6487  nnmsucr  6488  nnmcom  6489  nnsucsssuc  6492  nntri3or  6493  nnaordi  6508  nnaword  6511  nnmordi  6516  nnaordex  6528  ixpfn  6703  findcard  6887  findcard2  6888  findcard2s  6889  exmidomni  7139  indpi  7340  prarloclem3  7495  uzind4s2  9590  cnref1o  9649  frec2uzrdg  10408  expcl2lemap  10531  seq3coll  10821  climub  11351  climserle  11352  fsum3cvg  11385  summodclem2a  11388  prodfap0  11552  prodfrecap  11553  fproddccvg  11579  alginv  12046  algcvg  12047  algcvga  12050  algfx  12051  prmind2  12119  prmpwdvds  12352  lgsdir2lem4  14402