Theorem abeq2i 1567

Description: Equality of a class variable and a class abstraction (inference rule).

Hypothesis

Ref	Expression
abeqi.1	|- A = {x | ph}

Assertion

Ref	Expression
abeq2i	|- (x e. A <-> ph)

Proof of Theorem abeq2i

Step	Hyp	Ref	Expression
1		abeqi.1	. . 3 |- A = {x | ph}
2	1	eleq2i 1535	. 2 |- (x e. A <-> x e. {x | ph})
3		abid 1463	. 2 |- (x e. {x | ph} <-> ph)
4	2, 3	bitr 173	1 |- (x e. A <-> ph)

Syntax hints:   <-> wb 146   = wceq 954   e. wcel 956  {cab 1461

This theorem is referenced by:  rabid 1766  visset 1809  csbcog 2003  noel 2280  elpw 2400  elsn 2417  pw0 2464  snsspw 2475  elopab 2806  iunpw 2909  funcnv3 3550  zfrep6 3606  fv2 3711  tz6.12-1 3727  fopab2 3814  tfrlem4 3905  tfrlem5 3906  tfrlem8 3909  tfrlem9 3910  mapsnen 4416  sbthlem1 4433  ac6lem 4734  1pr 5097  1idpr 5113  ltexprlem1 5122  ltexprlem2 5123  ltexprlem3 5124  ltexprlem4 5125  ltexprlem6 5127  ltexprlem7 5128  reclem1pr 5136  reclem2pr 5137  reclem3pr 5138  reclem4pr 5139  suppsrlem 5201  suppsr3 5204  suprelem 5239  isbasis2g 7562  avril1 8723  chsscm 9051  chcmh 9052

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 961  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470

Copyright terms: Public domain