Theorem vtoclg 2798

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 2319	. 2 ⊢ Ⅎ𝑥𝐴
2		nfv 1528	. 2 ⊢ Ⅎ𝑥𝜓
3		vtoclg.1	. 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
4		vtoclg.2	. 2 ⊢ 𝜑
5	1, 2, 3, 4	vtoclgf 2796	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 2740

This theorem is referenced by:  vtoclbg  2799  ceqex  2865  mo2icl  2917  nelrdva  2945  sbctt  3030  sbcnestgf  3109  csbing  3343  ifmdc  3575  prnzg  3717  sneqrg  3763  unisng  3827  csbopabg  4082  trss  4111  inex1g  4140  ssexg  4143  pwexg  4181  prexg  4212  opth  4238  ordelord  4382  uniexg  4440  vtoclr  4675  resieq  4918  csbima12g  4990  dmsnsnsng  5107  iota5  5199  csbiotag  5210  funmo  5232  fconstg  5413  funfveu  5529  funbrfv  5555  fnbrfvb  5557  fvelimab  5573  ssimaexg  5579  fvelrn  5648  isoselem  5821  csbriotag  5843  csbov123g  5913  ovg  6013  tfrexlem  6335  rdg0g  6389  ensn1g  6797  fundmeng  6807  xpdom2g  6832  phplem3g  6856  prcdnql  7483  prcunqu  7484  prdisj  7491  shftvalg  10845  shftval4g  10846  climshft  11312  telfsumo  11474  fsumparts  11478  lcmgcdlem  12077  fiinopn  13507  bdzfauscl  14645  bdinex1g  14656  bdssexg  14659  bj-prexg  14666  bj-uniexg  14673