Theorem biabi 1181

Description: Equivalent wff's yield equal class abstractions (inference rule).

Hypothesis

Ref	Expression
biabi.1	|- (ph <-> ps)

Assertion

Ref	Expression
biabi	|- {x | ph} = {x | ps}

Proof of Theorem biabi

Step	Hyp	Ref	Expression
1		cleq2ab 1179	. 2 |- ({x | ph} = {x | ps} <-> A.x(ph <-> ps))
2		biabi.1	. 2 |- (ph <-> ps)
3	1, 2	mpgbir 686	1 |- {x | ph} = {x | ps}

Syntax hints:   <-> wb 127  {cab 1090   = wceq 1091

This theorem is referenced by:  birabi 1342  rabab 1359  elabs2 1457  zfrep4 1479  unrab 1694  difrab 1695  dfnul3 1710  pwpw0 1883  zfpair 1891  dfuni2 1921  unpr 1930  dfint2 1967  int0 1978  intmin2 1984  dfiun2 2014  dfiin2 2015  cbviunv 2016  cbvopab 2104  cbvopab1 2106  cbvopab1s 2107  cbvopab1v 2108  cbvopab2v 2109  unopab 2121  dfepfr 2184  epfrc 2185  dfom2 2374  dfdm3 2522  dfrn2 2523  dfrn3 2524  dfdm4 2525  dfdmf 2526  dmopab 2539  dmopabss 2540  dmopab2 2541  dm0 2542  dmsn0 2543  dmsnsn0 2544  dmi 2545  dfrnf 2561  rnopab 2566  dfima2 2604  dfima3 2605  imadmrn 2610  imai 2613  zfrep6 2744  fv2 2828  fvresex 2909  abrexexlem2 2911  abrexex2 2915  rdglem1 2975  rdglem2 2976  dfoprab2 3021  cbvoprab12 3028  dmoprab 3031  rnoprab 3033  oprvalex 3055  fo1st 3094  fo2nd 3095  ec2 3203  qsex 3231  snec 3232  ecid 3236  qsid 3237  map0e 3266  scottexs 3543  scott0s 3544  kardex 3550  aceq3 3556  cardval2 3661  cf0 3705  addcompr 3917  mulcompr 3919  sqr0 4730  infxpidmlem9 4941  infmap2lem1 4951  infmap2 4953

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-10 800  ax-11 801  ax-12 802  ax-16 922  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

metamath.org