Theorem abbii 2466

Description: Equivalent wff's yield equal class abstractions (inference rule). (Contributed by NM, 5-Aug-1993.)

Hypothesis

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

Assertion

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

Proof of Theorem abbii

Step	Hyp	Ref	Expression
1		abbi 2464	. 2 |- (A.x(ph <-> ps) <-> {x | ph} = {x | ps})
2		abbii.1	. 2 |- (ph <-> ps)
3	1, 2	mpgbi 1549	1 |- {x | ph} = {x | ps}

Syntax hints:   <-> wb 176   = wceq 1642  {cab 2339

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346

This theorem is referenced by:  rabswap  2791  rabbiia  2850  rabab  2877  csb2  3139  cbvcsb  3141  csbid  3144  csbco  3146  cbvreucsf  3201  unrab  3527  inrab  3528  inrab2  3529  difrab  3530  rabun2  3535  dfnul3  3554  rab0  3572  dfif2  3665  tprot  3816  pwpw0  3856  pwsn  3882  pwsnALT  3883  dfuni2  3894  dfint2  3929  int0  3941  cbviun  4004  cbviin  4005  iunrab  4014  iunid  4022  viin  4026  pw0  4161  dfiota2  4341  cbviota  4345  sb8iota  4347  addccom  4407  nncaddccl  4420  preaddccan2lem1  4455  ltfintrilem1  4466  dfevenfin2  4513  dfoddfin2  4514  nnadjoin  4521  tfinnn  4535  nulnnn  4557  phiun  4615  phialllem1  4617  opeq  4620  cbvopab  4631  cbvopab1  4633  cbvopab2  4634  cbvopab1s  4635  cbvopab2v  4637  unopab  4639  dfid3  4769  rabxp  4815  dfrn3  4904  dfdmf  4906  dmopab  4916  dmopabss  4917  dmopab3  4918  dfima4  4953  dfrnf  4963  rnopab  4968  rnopab2  4969  imadmrn  5009  imai  5011  epini  5022  iniseg  5023  iunfopab  5205  dfimafn2  5368  fvco2  5383  abrexco  5464  dfoprab2  5559  cbvoprab2  5569  dmoprab  5575  rnoprab  5577  rnoprab2  5578  fnrnov  5606  mptpreima  5683  dmmpt  5684  rnmpt2  5718  dfnnc3  5886  snec  5988  pmvalg  6011  map0e  6024  mapsn  6027  mucnc  6132  leconnnc  6219  addccan2nclem2  6265  nchoicelem16  6305