Theorem abbii 1622

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

Hypothesis

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

Assertion

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

Proof of Theorem abbii

Step	Hyp	Ref	Expression
1		eq2ab 1620	. 2 |- ({x | ph} = {x | ps} <-> A.x(ph <-> ps))
2		abbii.1	. 2 |- (ph <-> ps)
3	1, 2	mpgbir 1029	1 |- {x | ph} = {x | ps}

Syntax hints:   <-> wb 153   = wceq 997  {cab 1509

This theorem is referenced by:  rabswap 1818  rabbii 1852  rabab 1869  csbid 2056  unrab 2321  inrab 2322  inrab2 2323  difrab 2324  dfnul3 2334  dfif2 2415  pwpw0 2523  pwsn 2554  pwsnALT 2555  dfuni2 2559  unipr 2569  dfint2 2589  int0 2601  dfiin2 2642  cbviun 2643  viin 2661  iunun 2668  cbvopab 2727  cbvopab1 2729  cbvopab1s 2730  cbvopab2v 2732  unopab 2734  zfrep4 2756  abssexg 2803  zfpair 2833  dfid3 2892  uniuni 2937  dfepfr 2989  epfrc 2990  dfom2 3190  dfdm3 3359  dfrn2 3360  dfrn3 3361  dfdm4 3362  dfdmf 3363  dmopab 3377  dmopabss 3378  dmopab3 3379  dm0 3380  dmsn0 3381  dmsnsn0 3382  dmi 3383  dfrnf 3405  rnopab 3410  rnopab2 3411  dfima2 3462  dfima3 3463  imadmrn 3471  imai 3474  args 3485  zfrep6 3671  fv2 3777  dfimafn2 3819  fvresex 3914  abrexexlem2 3916  abrexex2 3928  abexssex 3929  abexex 3930  snnexOLD 3933  dfrdg2 3991  rdglem1 3995  rdglem2 3996  dfoprab2 4049  cbvoprab12 4056  dmoprab 4060  rnoprab 4062  fnrnoprval 4094  oprvalex 4099  fo1st 4149  fo2nd 4150  dfopab2 4171  oarec 4254  dfec2 4322  qsexg 4354  snec 4357  ecid 4361  qsid 4362  pmex 4388  map0e 4403  fiprlemOLD 4494  abfii1 4621  abfii2 4622  ruv 4661  scottexs 4780  scott0s 4781  kardex 4787  aceq3 4795  cardval2 4920  cf0 4975  addcompr 5188  mulcompr 5190  dfnn2 5996  sqr0 6762  sumex 7071  cbvsumi 7076  isumcl 7299  infxpidmlem9 7652  infmap2lem1 7671  infmap2 7673  tgval2 7706  iscau 8021  issubg 8200  minvecex 8662  efghgrpilem 8802  h2hcau 8932  hhlnoi 9909  nmopnegi 9972  nmop0 9993  nmfn0 9994  adjbdln 10099  foo3 10454  symgval 10488  symggrpi 10491  fiv 10571  hmeogrp 10632  subsp 10648  isalg 10735  algi 10742  ishomb 10798

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1003  ax-gen 1004  ax-8 1005  ax-10 1007  ax-12 1009  ax-17 1012  ax-4 1014  ax-5o 1016  ax-6o 1019  ax-9o 1164  ax-10o 1182  ax-16 1252  ax-11o 1260  ax-ext 1504

This theorem depends on definitions:  df-bi 154  df-an 232  df-ex 1022  df-sb 1214  df-clab 1510  df-cleq 1515  df-clel 1518

Copyright terms: Public domain