Theorem vtoclg 2832

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 2347	. 2 ⊢ Ⅎ𝑥𝐴
2		nfv 1550	. 2 ⊢ Ⅎ𝑥𝜓
3		vtoclg.1	. 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
4		vtoclg.2	. 2 ⊢ 𝜑
5	1, 2, 3, 4	vtoclgf 2830	1 ⊢ (𝐴 ∈ 𝑉 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1372   ∈ wcel 2175

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 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-v 2773

This theorem is referenced by:  vtoclbg  2833  ceqex  2899  mo2icl  2951  nelrdva  2979  sbctt  3064  sbcnestgf  3144  csbing  3379  ifmdc  3611  prnzg  3756  sneqrg  3802  unisng  3866  csbopabg  4121  trss  4150  inex1g  4179  ssexg  4182  pwexg  4223  prexg  4254  opth  4280  ordelord  4427  uniexg  4485  vtoclr  4722  resieq  4968  csbima12g  5042  dmsnsnsng  5159  iotaexab  5249  iota5  5252  csbiotag  5263  funmo  5285  fconstg  5471  funfveu  5588  funbrfv  5616  fnbrfvb  5618  fvelimab  5634  ssimaexg  5640  fvelrn  5710  isoselem  5888  csbriotag  5911  csbov123g  5982  ovg  6084  tfrexlem  6419  rdg0g  6473  ensn1g  6888  fundmeng  6898  xpdom2g  6926  phplem3g  6952  prcdnql  7596  prcunqu  7597  prdisj  7604  shftvalg  11118  shftval4g  11119  climshft  11586  telfsumo  11748  fsumparts  11752  lcmgcdlem  12370  fiinopn  14447  bdzfauscl  15788  bdinex1g  15799  bdssexg  15802  bj-prexg  15809  bj-uniexg  15816