Theorem vtoclg 1383

Description: Implicit substitution of a class for a set variable.

Hypotheses

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

Assertion

Ref	Expression
vtoclg	⊢ (A ∈ B → ψ)

Distinct variable group(s):   x,A   ψ,x

Proof of Theorem vtoclg

Step	Hyp	Ref	Expression
1		ax-17 925	. 2 ⊢ (y ∈ A → ∀x y ∈ A)
2		ax-17 925	. 2 ⊢ (ψ → ∀xψ)
3		vtoclg.1	. 2 ⊢ (x = A → (φ ↔ ψ))
4		vtoclg.2	. 2 ⊢ φ
5	1, 2, 3, 4	vtoclgf 1382	1 ⊢ (A ∈ B → ψ)

Syntax hints:   → wi 2   ↔ wb 127   = wceq 1091   ∈ wcel 1092

This theorem is referenced by:  vtoclbg 1384  vtoclga 1387  ceqex 1410  moeq3 1432  mo2icl 1434  inex1g 1699  ssexg 1702  elpwg 1802  pwexg 1807  snex 1859  prex 1892  opprc1b 1906  opth2 1909  unisng 1933  uniexg 1948  elintg 1973  trel 2048  trss 2050  efrirr 2180  ordelord 2221  sucidg 2305  vtoclr 2449  vtoclrbr 2450  vtoclibr 2451  resieq 2581  eliniseg 2618  funimaexg 2715  fneu 2728  fconstg 2775  tz6.12-2 2845  tz6.12i 2847  funopfvg 2854  fnfvbr 2855  fvelima 2859  fvelrn 2883  fvrn 2888  fvi 2900  abrexexg 2913  tfrlem10 2958  rdgzert 2982  domeng 3285  ensn1g 3330  en2sn 3336  snfi 3337  canth2g 3382  php2 3410  eirr 3450  tz9.13g 3508  rankvalg 3513  rankr1g 3519  r1pw 3529  ac7g 3570  numth2 3600  numthcor 3601  fodomg 3614  sucxpdom 3652  prnmax 3893

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-12 802  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-v 1349

metamath.org