Theorem rabbiia 3474

Description: Equivalent wff's 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 577	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑥 ∈ 𝐴 ∧ 𝜓))
3	2	abbii 2888	. 2 ⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)}
4		df-rab 3149	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
5		df-rab 3149	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)}
6	3, 4, 5	3eqtr4i 2856	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐴 ∣ 𝜓}

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1537   ∈ wcel 2114  {cab 2801  {crab 3144

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2124  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-sb 2070  df-clab 2802  df-cleq 2816  df-rab 3149

This theorem is referenced by:  rabbii  3475  fninfp  6938  fndifnfp  6940  nlimon  7568  dfom2  7584  rankval2  9249  ioopos  12816  prmreclem4  16257  acsfn1  16934  acsfn2  16936  logtayl  25245  ftalem3  25654  ppiub  25782  isuvtx  27179  vtxdginducedm1  27327  finsumvtxdg2size  27334  rgrusgrprc  27373  clwwlknclwwlkdif  27759  numclwwlkqhash  28156  ubthlem1  28649  xpinpreima  31151  xpinpreima2  31152  eulerpartgbij  31632  topdifinfeq  34633  rabimbieq  35515  rmydioph  39618  rmxdioph  39620  expdiophlem2  39626  expdioph  39627  alephiso3  39925  fsovrfovd  40362  k0004val0  40511  nzss  40656  hashnzfz  40659  fourierdlem90  42488  fourierdlem96  42494  fourierdlem97  42495  fourierdlem98  42496  fourierdlem99  42497  fourierdlem100  42498  fourierdlem109  42507  fourierdlem110  42508  fourierdlem112  42510  fourierdlem113  42511  sssmf  43022  dfodd6  43809  dfeven4  43810  dfeven2  43821  dfodd3  43822  dfeven3  43830  dfodd4  43831  dfodd5  43832