Theorem vtoclg 2883

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 105   = wceq 1402   ∈ wcel 2209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823

This theorem is used by:  vtoclbg  2884  ceqex  2953  mo2icl  3005  nelrdva  3033  sbctt  3118  sbcnestgf  3199  csbing  3438  ifmdc  3683  prnzg  3838  sneqrg  3887  unisng  3952  csbopabg  4209  trss  4238  sepg  4251  inex1g  4269  ssexg  4272  pwexg  4317  prexg  4349  opth  4377  ordelord  4526  uniexg  4585  vtoclr  4823  resieq  5073  csbima12g  5148  dmsnsnsng  5265  iotaexab  5356  iota5  5359  csbiotag  5370  funmo  5392  fconstg  5589  funfveu  5708  funbrfv  5739  fnbrfvb  5741  fvelimab  5759  ssimaexg  5765  fvelrn  5839  isoselem  6026  csbriotag  6052  csbov123g  6124  ovg  6228  tfrexlem  6605  rdg0g  6659  ensn1g  7084  fundmeng  7095  xpdom2g  7130  phplem3g  7157  prcdnql  7851  prcunqu  7852  prdisj  7859  shftvalg  11601  shftval4g  11602  climshft  12070  telfsumo  12233  fsumparts  12237  lcmgcdlem  12855  fiinopn  15105  bdsepg  16916  bdinex1g  16927  bdssexg  16930  bj-prexg  16937  bj-uniexg  16944