Theorem abbii 2465

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 2463	. 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  2790  rabbiia  2849  rabab  2876  csb2  3138  cbvcsb  3140  csbid  3143  csbco  3145  cbvreucsf  3200  unrab  3526  inrab  3527  inrab2  3528  difrab  3529  rabun2  3534  dfnul3  3553  rab0  3571  dfif2  3664  tprot  3815  pwpw0  3855  pwsn  3881  pwsnALT  3882  dfuni2  3893  dfint2  3928  int0  3940  cbviun  4003  cbviin  4004  iunrab  4013  iunid  4021  viin  4025  pw0  4160  dfiota2  4340  cbviota  4344  sb8iota  4346  addccom  4406  nncaddccl  4419  preaddccan2lem1  4454  ltfintrilem1  4465  dfevenfin2  4512  dfoddfin2  4513  nnadjoin  4520  tfinnn  4534  nulnnn  4556  phiun  4614  phialllem1  4616  opeq  4619  cbvopab  4630  cbvopab1  4632  cbvopab2  4633  cbvopab1s  4634  cbvopab2v  4636  unopab  4638  dfid3  4768  rabxp  4814  dfrn3  4903  dfdmf  4905  dmopab  4915  dmopabss  4916  dmopab3  4917  dfima4  4952  dfrnf  4962  rnopab  4967  rnopab2  4968  imadmrn  5008  imai  5010  epini  5021  iniseg  5022  iunfopab  5204  dfimafn2  5367  fvco2  5382  abrexco  5463  dfoprab2  5558  cbvoprab2  5568  dmoprab  5574  rnoprab  5576  rnoprab2  5577  fnrnov  5605  mptpreima  5682  dmmpt  5683  rnmpt2  5717  dfnnc3  5885  snec  5987  pmvalg  6010  map0e  6023  mapsn  6026  mucnc  6131  leconnnc  6218  addccan2nclem2  6264  nchoicelem16  6304