Theorem vtoclg 2682

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

Syntax hints:   → wi 4   ↔ wb 104   = wceq 1290   ∈ wcel 1439

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 666  ax-5 1382  ax-7 1383  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-8 1441  ax-10 1442  ax-11 1443  ax-i12 1444  ax-bndl 1445  ax-4 1446  ax-17 1465  ax-i9 1469  ax-ial 1473  ax-i5r 1474  ax-ext 2071

This theorem depends on definitions:  df-bi 116  df-tru 1293  df-nf 1396  df-sb 1694  df-clab 2076  df-cleq 2082  df-clel 2085  df-nfc 2218  df-v 2624

This theorem is referenced by:  vtoclbg  2683  ceqex  2747  mo2icl  2797  nelrdva  2825  sbctt  2908  sbcnestgf  2982  csbing  3210  ifmdc  3434  prnzg  3572  sneqrg  3614  unisng  3678  csbopabg  3924  trss  3953  inex1g  3983  ssexg  3986  pwexg  4023  prexg  4049  opth  4075  ordelord  4219  uniexg  4277  vtoclr  4501  resieq  4738  csbima12g  4808  dmsnsnsng  4923  iota5  5015  csbiotag  5023  funmo  5045  fconstg  5222  funfveu  5333  funbrfv  5358  fnbrfvb  5360  fvelimab  5375  ssimaexg  5381  fvelrn  5446  isoselem  5615  csbriotag  5636  csbov123g  5703  ovg  5799  tfrexlem  6115  rdg0g  6169  ensn1g  6570  fundmeng  6580  xpdom2g  6604  phplem3g  6628  prcdnql  7106  prcunqu  7107  prdisj  7114  shftvalg  10333  shftval4g  10334  climshft  10755  telfsumo  10923  fsumparts  10927  lcmgcdlem  11400  fiinopn  11766  bdzfauscl  12085  bdinex1g  12096  bdssexg  12099  bj-prexg  12106  bj-uniexg  12113