Theorem rabbiia 3160

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 666	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑥 ∈ 𝐴 ∧ 𝜓))
3	2	abbii 2725	. 2 ⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)}
4		df-rab 2904	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
5		df-rab 2904	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)}
6	3, 4, 5	3eqtr4i 2641	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐴 ∣ 𝜓}

Syntax hints:   → wi 4   ↔ wb 194   ∧ wa 382   = wceq 1474   ∈ wcel 1976  {cab 2595  {crab 2899

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589

This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-rab 2904

This theorem is referenced by:  elneldisj  3916  elnelun  3917  dfepfr  5013  epfrc  5014  fndmdifcom  6215  fniniseg2  6233  fninfp  6323  fndifnfp  6325  bm2.5ii  6876  nlimon  6921  dfom2  6937  dfoi  8277  rankval2  8542  kmlem3  8835  alephsuc3  9259  ioopos  12080  hashbclem  13048  gcdcom  15022  gcdass  15051  lcmcom  15093  lcmass  15114  prmreclem4  15410  acsfn0  16093  acsfn1  16094  acsfn2  16096  dfrhm2  18489  lbsextg  18932  fctop2  20567  ordtrest2  20766  qtopres  21259  tsmsfbas  21689  shftmbl  23058  logtayl  24151  ftalem3  24546  ppiub  24674  rpvmasum  24960  usgrafilem1  25734  clwlknclwlkdifs  26281  numclwwlkovf2num  26406  ubthlem1  26944  fpwrelmapffslem  28729  xpinpreima  29114  xpinpreima2  29115  ordtrest2NEW  29131  unelldsys  29382  rossros  29404  aean  29468  eulerpartgbij  29595  orvcval2  29681  subfacp1lem6  30255  bj-dmtopon  32066  topdifinfeq  32198  itg2addnclem2  32456  scottexf  32970  scott0f  32971  glbconxN  33506  3anrabdioph  36188  3orrabdioph  36189  rexrabdioph  36200  2rexfrabdioph  36202  3rexfrabdioph  36203  4rexfrabdioph  36204  6rexfrabdioph  36205  7rexfrabdioph  36206  elnn0rabdioph  36209  elnnrabdioph  36213  rabren3dioph  36221  rmydioph  36423  rmxdioph  36425  expdiophlem2  36431  expdioph  36432  relintab  36732  fsovrfovd  37147  k0004val0  37296  nzss  37362  hashnzfz  37365  uzmptshftfval  37391  binomcxplemdvsum  37400  binomcxp  37402  dvnprod  38663  fourierdlem90  38913  fourierdlem96  38919  fourierdlem97  38920  fourierdlem98  38921  fourierdlem99  38922  fourierdlem100  38923  fourierdlem109  38932  fourierdlem110  38933  fourierdlem112  38935  fourierdlem113  38936  ovnsubadd  39286  hoidmv1lelem3  39307  hoidmvlelem3  39311  ovolval3  39361  ovolval4lem2  39364  ovolval5lem3  39368  sssmf  39449  smflimlem4  39484  dfodd6  39913  dfeven4  39914  dfeven2  39925  dfodd3  39926  dfeven3  39933  dfodd4  39934  dfodd5  39935  umgrislfupgrlem  40369  rgrusgrprc  40811  clwwlknclwwlkdifs  41203  av-numclwwlkovf2num  41538