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  6605  fndifnfp  6607  nlimon  7217  dfom2  7233  rankval2  8856  ioopos  12463  prmreclem4  15845  acsfn1  16543  acsfn2  16545  logtayl  24626  ftalem3  25021  ppiub  25149  isuvtx  26518  vtxdginducedm1  26670  finsumvtxdg2size  26677  rgrusgrprc  26716  clwwlknclwwlkdif  27121  clwwlknclwwlkdifsOLD  27123  numclwwlkqhash  27557  ubthlem1  28056  xpinpreima  30282  xpinpreima2  30283  eulerpartgbij  30764  topdifinfeq  33527  rabimbieq  34358  rmydioph  38101  rmxdioph  38103  expdiophlem2  38109  expdioph  38110  fsovrfovd  38823  k0004val0  38972  nzss  39036  hashnzfz  39039  fourierdlem90  40934  fourierdlem96  40940  fourierdlem97  40941  fourierdlem98  40942  fourierdlem99  40943  fourierdlem100  40944  fourierdlem109  40953  fourierdlem110  40954  fourierdlem112  40956  fourierdlem113  40957  sssmf  41471  dfodd6  42078  dfeven4  42079  dfeven2  42090  dfodd3  42091  dfeven3  42098  dfodd4  42099  dfodd5  42100