Theorem abbii 1618

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

Syntax hints:   <-> wb 144   = wceq 992  {cab 1505

This theorem is referenced by:  rabswap 1817  rabbii 1851  rabab 1868  csbid 2056  unrab 2322  inrab 2323  inrab2 2324  difrab 2325  dfnul3 2335  dfif2 2417  pwpw0 2533  pwsn 2565  pwsnALT 2566  pwpr 2567  dfuni2 2571  unipr 2581  dfint2 2602  int0 2614  dfiin2 2656  cbviun 2657  iunid 2671  viin 2675  iunun 2683  cbvopab 2746  cbvopab1 2748  cbvopab1s 2749  cbvopab2v 2751  unopab 2753  zfrep4 2775  abssexg 2825  zfpair 2853  dfid3 2914  dfepfr 2960  epfrc 2961  uniuni 3104  dfom2 3220  dfdm3 3393  dfrn2 3394  dfrn3 3395  dfdm4 3396  dfdmf 3397  dmopab 3411  dmopabss 3412  dmopab3 3413  dm0 3414  dmi 3415  dfrnf 3435  rnopab 3440  rnopab2 3441  dfima2 3497  dfima3 3498  imadmrn 3506  imai 3509  args 3520  zfrep6 3721  fv2 3831  dfimafn2 3873  fvresex 3971  abrexexlem2 3973  abrexex2 3985  abexssex 3986  abexex 3987  dfoprab2 4050  cbvoprab1 4057  cbvoprab12 4058  dmoprab 4062  rnoprab 4064  fnrnoprv 4097  oprvex 4102  fo1st 4152  fo2nd 4153  dfopab2 4173  fparlem1 4199  fparlem2 4200  dfrdg2 4234  rdglem1 4238  rdglem2 4239  oarec 4332  dfec2 4404  qsexg 4434  snec 4437  ecid 4441  qsid 4442  pmex 4468  map0e 4483  abfii1 4704  abfii2 4705  ruv 4744  scottexs 4864  scott0s 4865  kardex 4871  aceq3 4879  cardval2 5005  cf0 5060  addcompr 5277  mulcompr 5279  dfnn2 6081  sqr0 6873  sumex 7184  cbvsumi 7189  isumcl 7413  infxpidmlem9 7772  infmap2lem1 7791  infmap2 7793  tgval2 7829  iscau 8147  issubg 8358  minvecex 8838  efghgrpilem 8991  h2hcau 9124  hhlnoi 10106  nmopnegi 10168  nmop0 10189  nmfn0 10190  adjbdln 10295  foo3 10652  symgval 10688  symggrpi 10691  fiv 10849  zrdivrng 10969  hmeogrp 11044  subsp 11056  subspemp 11060  clindistop 11131  singempcon 11134  isalg 11175  algi 11181  ishomb 11243  cbviin 11401  fictblem 11422  fictb 11423  neibastop2lem1 11580  neibastop2lem4 11583  oprabopabf 11807  cbvixpv 11821  abrexex2g 11825  abrexdom 11826  firnfi3 11830  heiborlem8 12018  ismrer1 12080

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-10 1002  ax-12 1004  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500

This theorem depends on definitions:  df-bi 145  df-an 223  df-ex 1017  df-sb 1209  df-clab 1506  df-cleq 1511  df-clel 1514

Copyright terms: Public domain