Theorem vtoclga 2796

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

Syntax hints:   → wi 4   ↔ wb 104   = wceq 1348   ∈ wcel 2141

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-v 2732

This theorem is referenced by:  vtoclri  2805  ssuni  3818  ordtriexmid  4505  onsucsssucexmid  4511  tfis3  4570  fvmpt3  5575  fvmptssdm  5580  fnressn  5682  fressnfv  5683  caovord  6024  caovimo  6046  tfrlem1  6287  nnacl  6459  nnmcl  6460  nnacom  6463  nnaass  6464  nndi  6465  nnmass  6466  nnmsucr  6467  nnmcom  6468  nnsucsssuc  6471  nntri3or  6472  nnaordi  6487  nnaword  6490  nnmordi  6495  nnaordex  6507  ixpfn  6682  findcard  6866  findcard2  6867  findcard2s  6868  exmidomni  7118  indpi  7304  prarloclem3  7459  uzind4s2  9550  cnref1o  9609  frec2uzrdg  10365  expcl2lemap  10488  seq3coll  10777  climub  11307  climserle  11308  fsum3cvg  11341  summodclem2a  11344  prodfap0  11508  prodfrecap  11509  fproddccvg  11535  alginv  12001  algcvg  12002  algcvga  12005  algfx  12006  prmind2  12074  prmpwdvds  12307  lgsdir2lem4  13726