Theorem rabbiia 3396

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   = wceq 1539   ∈ wcel 2108  {cab 2715  {crab 3067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-rab 3072

This theorem is referenced by:  rabbii  3397  fninfp  7028  fndifnfp  7030  nlimon  7673  dfom2  7689  rankval2  9507  ioopos  13085  prmreclem4  16548  acsfn1  17287  acsfn2  17289  logtayl  25720  ftalem3  26129  ppiub  26257  isuvtx  27665  vtxdginducedm1  27813  finsumvtxdg2size  27820  rgrusgrprc  27859  clwwlknclwwlkdif  28244  numclwwlkqhash  28640  ubthlem1  29133  xpinpreima  31758  xpinpreima2  31759  eulerpartgbij  32239  topdifinfeq  35448  rabimbieq  36318  rmydioph  40752  rmxdioph  40754  expdiophlem2  40760  expdioph  40761  alephiso3  41055  fsovrfovd  41506  k0004val0  41653  nzss  41824  hashnzfz  41827  fourierdlem90  43627  fourierdlem96  43633  fourierdlem97  43634  fourierdlem98  43635  fourierdlem99  43636  fourierdlem100  43637  fourierdlem109  43646  fourierdlem110  43647  fourierdlem112  43649  fourierdlem113  43650  sssmf  44161  dfodd6  44977  dfeven4  44978  dfeven2  44989  dfodd3  44990  dfeven3  44998  dfodd4  44999  dfodd5  45000