Theorem vtoclg 2584

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

Hypotheses

Ref	Expression
vtoclg.1	⊢ (x = A → (φ ↔ ψ))
vtoclg.2	⊢ φ

Assertion

Ref	Expression
vtoclg	⊢ (A ∈ 𝑉 → ψ)

Distinct variable groups:   x,A   ψ,x

Allowed substitution hints:   φ(x)   𝑉(x)

Proof of Theorem vtoclg

Step	Hyp	Ref	Expression
1		nfcv 2154	. 2 ⊢ ℲxA
2		nfv 1397	. 2 ⊢ Ⅎxψ
3		vtoclg.1	. 2 ⊢ (x = A → (φ ↔ ψ))
4		vtoclg.2	. 2 ⊢ φ
5	1, 2, 3, 4	vtoclgf 2583	1 ⊢ (A ∈ 𝑉 → ψ)

Syntax hints:   → wi 4   ↔ wb 98   = wceq 1226   ∈ wcel 1369

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 614  ax-5 1312  ax-7 1313  ax-gen 1314  ax-ie1 1358  ax-ie2 1359  ax-8 1371  ax-10 1372  ax-11 1373  ax-i12 1374  ax-bnd 1375  ax-4 1376  ax-17 1395  ax-i9 1399  ax-ial 1403  ax-i5r 1404  ax-ext 1998

This theorem depends on definitions:  df-bi 110  df-tru 1229  df-nf 1326  df-sb 1622  df-clab 2003  df-cleq 2009  df-clel 2012  df-nfc 2143  df-v 2531

This theorem is referenced by:  vtoclbg  2585  ceqex  2642  mo2icl  2691  nelrdva  2717  sbctt  2795  sbcnestgf  2868  csbing  3115  prnzg  3458  sneqrg  3499  unisng  3563  csbopabg  3801  trss  3829  inex1g  3859  ssexg  3862  pwexg  3899  prexgOLD  3912  prexg  3913  opth  3940  ordelord  4059  uniexg  4116  vtoclr  4306  resieq  4540  csbima12g  4604  dmsnsnsng  4716  iota5  4805  csbiotag  4813  funmo  4834  fconstg  4999  funfveu  5104  funbrfv  5128  fnbrfvb  5130  fvelimab  5145  ssimaexg  5151  fvelrn  5214  isoselem  5375  csbriotag  5395  csbov123g  5457  ovg  5553  tfrexlem  5861  prcdnql  6327  prcunqu  6328  prdisj  6335  bdzfauscl  8530  bdinex1g  8538  bdssexg  8541  bj-prexg  8548  bj-uniexg  8555