Theorem rabbiia 3419

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2111  {cab 2776  {crab 3110

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-rab 3115

This theorem is referenced by:  rabbii  3420  fninfp  6913  fndifnfp  6915  nlimon  7546  dfom2  7562  rankval2  9231  ioopos  12802  prmreclem4  16245  acsfn1  16924  acsfn2  16926  logtayl  25251  ftalem3  25660  ppiub  25788  isuvtx  27185  vtxdginducedm1  27333  finsumvtxdg2size  27340  rgrusgrprc  27379  clwwlknclwwlkdif  27764  numclwwlkqhash  28160  ubthlem1  28653  xpinpreima  31259  xpinpreima2  31260  eulerpartgbij  31740  topdifinfeq  34767  rabimbieq  35673  rmydioph  39955  rmxdioph  39957  expdiophlem2  39963  expdioph  39964  alephiso3  40258  fsovrfovd  40710  k0004val0  40857  nzss  41021  hashnzfz  41024  fourierdlem90  42838  fourierdlem96  42844  fourierdlem97  42845  fourierdlem98  42846  fourierdlem99  42847  fourierdlem100  42848  fourierdlem109  42857  fourierdlem110  42858  fourierdlem112  42860  fourierdlem113  42861  sssmf  43372  dfodd6  44155  dfeven4  44156  dfeven2  44167  dfodd3  44168  dfeven3  44176  dfodd4  44177  dfodd5  44178