Theorem rabbiia 3324

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

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   = wceq 1632   ∈ wcel 2139  {cab 2746  {crab 3054

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-rab 3059

This theorem is referenced by:  rabbii  3325  elneldisjOLD  4108  elnelunOLD  4109  fninfp  6604  fndifnfp  6606  nlimon  7216  dfom2  7232  rankval2  8854  ioopos  12443  prmreclem4  15825  acsfn1  16523  acsfn2  16525  logtayl  24605  ftalem3  25000  ppiub  25128  isuvtx  26497  vtxdginducedm1  26649  finsumvtxdg2size  26656  rgrusgrprc  26695  clwwlknclwwlkdif  27100  clwwlknclwwlkdifsOLD  27102  numclwwlkqhash  27536  ubthlem1  28035  xpinpreima  30261  xpinpreima2  30262  eulerpartgbij  30743  topdifinfeq  33509  rabimbieq  34340  rmydioph  38083  rmxdioph  38085  expdiophlem2  38091  expdioph  38092  fsovrfovd  38805  k0004val0  38954  nzss  39018  hashnzfz  39021  fourierdlem90  40916  fourierdlem96  40922  fourierdlem97  40923  fourierdlem98  40924  fourierdlem99  40925  fourierdlem100  40926  fourierdlem109  40935  fourierdlem110  40936  fourierdlem112  40938  fourierdlem113  40939  sssmf  41453  dfodd6  42060  dfeven4  42061  dfeven2  42072  dfodd3  42073  dfeven3  42080  dfodd4  42081  dfodd5  42082