Theorem abbii 1572

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 1570	. 2 |- ({x | ph} = {x | ps} <-> A.x(ph <-> ps))
2		abbii.1	. 2 |- (ph <-> ps)
3	1, 2	mpgbir 986	1 |- {x | ph} = {x | ps}

Syntax hints:   <-> wb 146   = wceq 954  {cab 1461

This theorem is referenced by:  rabswap 1768  rabbii 1801  rabab 1818  csbid 2001  unrab 2266  inrab 2267  inrab2 2268  difrab 2269  dfnul3 2279  dfif2 2359  pwpw0 2465  pwsn 2496  dfuni2 2500  unipr 2510  dfint2 2530  int0 2542  dfiin2 2583  cbviun 2584  iunun 2608  cbvopab 2667  cbvopab1 2669  cbvopab1s 2670  cbvopab2v 2672  unopab 2674  zfrep4 2696  abssexg 2742  zfpair 2772  dfid3 2831  uniuni 2875  dfepfr 2927  epfrc 2928  dfom2 3128  dfdm3 3297  dfrn2 3298  dfrn3 3299  dfdm4 3300  dfdmf 3301  dmopab 3315  dmopabss 3316  dmopab3 3317  dm0 3318  dmsn0 3319  dmsnsn0 3320  dmi 3321  dfrnf 3342  rnopab 3347  rnopab2 3348  dfima2 3397  dfima3 3398  imadmrn 3406  imai 3409  args 3420  zfrep6 3606  fv2 3711  dfimafn2 3753  fvresex 3848  abrexexlem2 3850  abrexex2 3862  abexssex 3863  abexex 3864  dfrdg2 3924  rdglem1 3928  rdglem2 3929  dfoprab2 3982  cbvoprab12 3989  dmoprab 3993  rnoprab 3995  fnrnoprval 4027  oprvalex 4032  fo1st 4081  fo2nd 4082  dfopab2 4103  oarec 4186  dfec2 4254  qsexg 4284  snec 4286  ecid 4290  qsid 4291  pmex 4317  map0e 4332  abfii1 4541  abfii2 4542  scottexs 4698  scott0s 4699  kardex 4705  aceq3 4713  cardval2 4835  cf0 4890  addcompr 5103  mulcompr 5105  dfnn2 5892  sqr0 6610  sumex 6927  cbvsum 6932  isumclt 7152  infxpidmlem9 7511  infmap2lem1 7529  infmap2 7531  tgval2t 7567  fctop2 7601  iscau 7888  issubg 8068  minvecex 8522  efghgrpilem 8653  h2hcau 8788  hhlno 9766  nmopneg 9828  nmop0 9849  nmfn0 9850  adjbdlnt 9954  symgval 10337  symggrpi 10340  fiv 10410  hmeogrp 10461  subsp 10465  isalg 10533  algi 10540  ishomb 10596

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  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