Theorem abbii 1567

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

Syntax hints:   <-> wb 146   = wceq 953  {cab 1456

This theorem is referenced by:  rabswap 1763  rabbii 1796  rabab 1813  csbid 1995  unrab 2260  inrab 2261  inrab2 2262  difrab 2263  dfnul3 2273  dfif2 2353  pwpw0 2460  pwsn 2491  dfuni2 2495  unipr 2505  dfint2 2525  int0 2537  dfiin2 2578  cbviun 2579  iunun 2603  cbvopab 2662  cbvopab1 2664  cbvopab1s 2665  cbvopab2v 2667  unopab 2669  zfrep4 2691  abssexg 2737  zfpair 2767  dfid3 2826  uniuni 2870  dfepfr 2922  epfrc 2923  dfom2 3123  dfdm3 3291  dfrn2 3292  dfrn3 3293  dfdm4 3294  dfdmf 3295  dmopab 3309  dmopabss 3310  dmopab3 3311  dm0 3312  dmsn0 3313  dmsnsn0 3314  dmi 3315  dfrnf 3334  rnopab 3339  rnopab2 3340  dfima2 3389  dfima3 3390  imadmrn 3398  imai 3401  args 3412  zfrep6 3600  fv2 3705  dfimafn2 3747  fvresex 3842  abrexexlem2 3844  abrexex2 3856  abexssex 3857  abexex 3858  dfrdg2 3918  rdglem1 3922  rdglem2 3923  dfoprab2 3976  cbvoprab12 3983  dmoprab 3987  rnoprab 3989  fnrnoprval 4021  oprvalex 4026  fo1st 4075  fo2nd 4076  dfopab2 4097  oarec 4180  dfec2 4248  qsexg 4278  snec 4280  ecid 4284  qsid 4285  pmex 4311  map0e 4326  abfii1 4535  abfii2 4536  scottexs 4690  scott0s 4691  kardex 4697  aceq3 4705  cardval2 4827  cf0 4882  addcompr 5095  mulcompr 5097  dfnn2 5884  sqr0 6602  sumex 6919  cbvsum 6924  isumclt 7144  infxpidmlem9 7503  infmap2lem1 7521  infmap2 7523  tgval2t 7559  fctop2 7593  iscau 7874  issubg 8053  minvecex 8509  efghgrpilem 8634  h2hcau 8788  hhlno 9743  nmopneg 9805  nmop0 9826  nmfn0 9827  adjbdlnt 9931  symgval 10308  symggrpiOLD 10311  symggrpi 10313  fiv 10374  hmeogrp 10425  subsp 10429  isalg 10497  algi 10504  ishomb 10560

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-12 965  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978  df-sb 1168  df-clab 1457  df-cleq 1462  df-clel 1465

Copyright terms: Public domain