Theorem rabbiia 3407

Description: Equivalent formulas yield equal restricted class abstractions (inference form). (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 575	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑥 ∈ 𝐴 ∧ 𝜓))
3	2	abbii 2808	. 2 ⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)}
4		df-rab 3073	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
5		df-rab 3073	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)}
6	3, 4, 5	3eqtr4i 2776	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐴 ∣ 𝜓}

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1539   ∈ wcel 2106  {cab 2715  {crab 3068

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-rab 3073

This theorem is referenced by:  rabbii  3408  fninfp  7046  fndifnfp  7048  nlimon  7698  dfom2  7714  rankval2  9576  ioopos  13156  prmreclem4  16620  acsfn1  17370  acsfn2  17372  logtayl  25815  ftalem3  26224  ppiub  26352  isuvtx  27762  vtxdginducedm1  27910  finsumvtxdg2size  27917  rgrusgrprc  27956  clwwlknclwwlkdif  28343  numclwwlkqhash  28739  ubthlem1  29232  xpinpreima  31856  xpinpreima2  31857  eulerpartgbij  32339  topdifinfeq  35521  rabimbieq  36391  rmydioph  40836  rmxdioph  40838  expdiophlem2  40844  expdioph  40845  alephiso3  41166  fsovrfovd  41617  k0004val0  41764  nzss  41935  hashnzfz  41938  fourierdlem90  43737  fourierdlem96  43743  fourierdlem97  43744  fourierdlem98  43745  fourierdlem99  43746  fourierdlem100  43747  fourierdlem109  43756  fourierdlem110  43757  fourierdlem112  43759  fourierdlem113  43760  sssmf  44274  dfodd6  45089  dfeven4  45090  dfeven2  45101  dfodd3  45102  dfeven3  45110  dfodd4  45111  dfodd5  45112