Theorem rabbiia 3161

Description: Equivalent wff's yield equal restricted class abstractions (inference rule). (Contributed by NM, 22-May-1999.)

Hypothesis

Ref	Expression
rabbiia.1	⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
rabbiia	⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐴 ∣ 𝜓}

Proof of Theorem rabbiia

Step	Hyp	Ref	Expression
1		rabbiia.1	. . . 4 ⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝜓))
2	1	pm5.32i 667	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑥 ∈ 𝐴 ∧ 𝜓))
3	2	abbii 2726	. 2 ⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)}
4		df-rab 2905	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
5		df-rab 2905	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)}
6	3, 4, 5	3eqtr4i 2642	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐴 ∣ 𝜓}

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475   ∈ wcel 1977  {cab 2596  {crab 2900

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-rab 2905

This theorem is referenced by:  elneldisj  3917  elnelun  3918  dfepfr  5023  epfrc  5024  fndmdifcom  6230  fniniseg2  6248  fninfp  6345  fndifnfp  6347  bm2.5ii  6898  nlimon  6943  dfom2  6959  dfoi  8299  rankval2  8564  kmlem3  8857  alephsuc3  9281  ioopos  12121  hashbclem  13093  gcdcom  15073  gcdass  15102  lcmcom  15144  lcmass  15165  prmreclem4  15461  acsfn0  16144  acsfn1  16145  acsfn2  16147  dfrhm2  18540  lbsextg  18983  fctop2  20619  ordtrest2  20818  qtopres  21311  tsmsfbas  21741  shftmbl  23113  logtayl  24206  ftalem3  24601  ppiub  24729  rpvmasum  25015  umgrislfupgrlem  25788  usgrafilem1  25940  clwlknclwlkdifs  26487  numclwwlkovf2num  26612  ubthlem1  27110  fpwrelmapffslem  28895  xpinpreima  29280  xpinpreima2  29281  ordtrest2NEW  29297  unelldsys  29548  rossros  29570  aean  29634  eulerpartgbij  29761  orvcval2  29847  subfacp1lem6  30421  bj-dmtopon  32242  topdifinfeq  32374  itg2addnclem2  32632  scottexf  33146  scott0f  33147  glbconxN  33682  3anrabdioph  36364  3orrabdioph  36365  rexrabdioph  36376  2rexfrabdioph  36378  3rexfrabdioph  36379  4rexfrabdioph  36380  6rexfrabdioph  36381  7rexfrabdioph  36382  elnn0rabdioph  36385  elnnrabdioph  36389  rabren3dioph  36397  rmydioph  36599  rmxdioph  36601  expdiophlem2  36607  expdioph  36608  relintab  36908  fsovrfovd  37323  k0004val0  37472  nzss  37538  hashnzfz  37541  uzmptshftfval  37567  binomcxplemdvsum  37576  binomcxp  37578  dvnprod  38839  fourierdlem90  39089  fourierdlem96  39095  fourierdlem97  39096  fourierdlem98  39097  fourierdlem99  39098  fourierdlem100  39099  fourierdlem109  39108  fourierdlem110  39109  fourierdlem112  39111  fourierdlem113  39112  ovnsubadd  39462  hoidmv1lelem3  39483  hoidmvlelem3  39487  ovolval3  39537  ovolval4lem2  39540  ovolval5lem3  39544  sssmf  39625  smflimlem4  39660  dfodd6  40088  dfeven4  40089  dfeven2  40100  dfodd3  40101  dfeven3  40108  dfodd4  40109  dfodd5  40110  rgrusgrprc  40789  clwwlknclwwlkdifs  41181  av-numclwwlkovf2num  41516