Theorem vtoclg 2812

Description: Implicit substitution of a class expression for a setvar variable. (Contributed by NM, 17-Apr-1995.)

Hypotheses

Ref	Expression
vtoclg.1	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
vtoclg.2	⊢ 𝜑

Assertion

Ref	Expression
vtoclg	⊢ (𝐴 ∈ 𝑉 → 𝜓)

Distinct variable groups:   𝑥,𝐴   𝜓,𝑥

Allowed substitution hints:   𝜑(𝑥)   𝑉(𝑥)

Proof of Theorem vtoclg

Step	Hyp	Ref	Expression
1		nfcv 2332	. 2 ⊢ Ⅎ𝑥𝐴
2		nfv 1539	. 2 ⊢ Ⅎ𝑥𝜓
3		vtoclg.1	. 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
4		vtoclg.2	. 2 ⊢ 𝜑
5	1, 2, 3, 4	vtoclgf 2810	1 ⊢ (𝐴 ∈ 𝑉 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1364   ∈ wcel 2160

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-v 2754

This theorem is referenced by:  vtoclbg  2813  ceqex  2879  mo2icl  2931  nelrdva  2959  sbctt  3044  sbcnestgf  3123  csbing  3357  ifmdc  3589  prnzg  3731  sneqrg  3777  unisng  3841  csbopabg  4096  trss  4125  inex1g  4154  ssexg  4157  pwexg  4195  prexg  4226  opth  4252  ordelord  4396  uniexg  4454  vtoclr  4689  resieq  4932  csbima12g  5004  dmsnsnsng  5121  iota5  5213  csbiotag  5224  funmo  5246  fconstg  5427  funfveu  5543  funbrfv  5570  fnbrfvb  5572  fvelimab  5588  ssimaexg  5594  fvelrn  5663  isoselem  5837  csbriotag  5859  csbov123g  5929  ovg  6030  tfrexlem  6353  rdg0g  6407  ensn1g  6815  fundmeng  6825  xpdom2g  6850  phplem3g  6874  prcdnql  7501  prcunqu  7502  prdisj  7509  shftvalg  10863  shftval4g  10864  climshft  11330  telfsumo  11492  fsumparts  11496  lcmgcdlem  12095  fiinopn  13888  bdzfauscl  15026  bdinex1g  15037  bdssexg  15040  bj-prexg  15047  bj-uniexg  15054