Theorem abbii 1578

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

Syntax hints:   <-> wb 146   = wceq 958  {cab 1466

This theorem is referenced by:  rabswap 1774  rabbii 1808  rabab 1825  csbid 2008  unrab 2273  inrab 2274  inrab2 2275  difrab 2276  dfnul3 2286  dfif2 2367  pwpw0 2473  pwsn 2504  pwsnALT 2505  dfuni2 2509  unipr 2519  dfint2 2539  int0 2551  dfiin2 2592  cbviun 2593  viin 2611  iunun 2618  cbvopab 2677  cbvopab1 2679  cbvopab1s 2680  cbvopab2v 2682  unopab 2684  zfrep4 2706  abssexg 2753  zfpair 2783  dfid3 2842  uniuni 2886  dfepfr 2938  epfrc 2939  dfom2 3139  dfdm3 3308  dfrn2 3309  dfrn3 3310  dfdm4 3311  dfdmf 3312  dmopab 3326  dmopabss 3327  dmopab3 3328  dm0 3329  dmsn0 3330  dmsnsn0 3331  dmi 3332  dfrnf 3354  rnopab 3359  rnopab2 3360  dfima2 3411  dfima3 3412  imadmrn 3420  imai 3423  args 3434  zfrep6 3620  fv2 3726  dfimafn2 3768  fvresex 3863  abrexexlem2 3865  abrexex2 3877  abexssex 3878  abexex 3879  dfrdg2 3939  rdglem1 3943  rdglem2 3944  dfoprab2 3997  cbvoprab12 4004  dmoprab 4008  rnoprab 4010  fnrnoprval 4042  oprvalex 4047  fo1st 4097  fo2nd 4098  dfopab2 4119  oarec 4202  dfec2 4270  qsexg 4300  snec 4302  ecid 4306  qsid 4307  pmex 4333  map0e 4348  abfii1OLD 4574  scottexs 4728  scott0s 4729  kardex 4735  aceq3 4743  cardval2 4866  cf0 4922  addcompr 5135  mulcompr 5137  dfnn2 5938  sqr0 6673  sumex 6981  cbvsum 6986  isumclt 7209  infxpidmlem9 7561  infmap2lem1 7581  infmap2 7583  tgval2t 7616  fctop2OLD 7648  iscau 7933  issubg 8112  minvecex 8574  efghgrpilem 8714  h2hcau 8844  hhlno 9821  nmopneg 9884  nmop0 9905  nmfn0 9906  adjbdlnt 10011  symgval 10398  symggrpi 10401  fiv 10470  hmeogrp 10524  subsp 10540  isalg 10624  algi 10631  ishomb 10687

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475

Copyright terms: Public domain