Theorem rabbiia 3385

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 2824	. 2 ⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)}
4		df-rab 3080	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
5		df-rab 3080	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)}
6	3, 4, 5	3eqtr4i 2792	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐴 ∣ 𝜓}

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1539   ∈ wcel 2112  {cab 2736  {crab 3075

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 1912  ax-6 1971  ax-7 2016  ax-9 2122  ax-ext 2730

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1783  df-sb 2071  df-clab 2737  df-cleq 2751  df-rab 3080

This theorem is referenced by:  rabbii  3386  fninfp  6934  fndifnfp  6936  nlimon  7572  dfom2  7588  rankval2  9294  ioopos  12870  prmreclem4  16325  acsfn1  17005  acsfn2  17007  logtayl  25365  ftalem3  25774  ppiub  25902  isuvtx  27299  vtxdginducedm1  27447  finsumvtxdg2size  27454  rgrusgrprc  27493  clwwlknclwwlkdif  27878  numclwwlkqhash  28274  ubthlem1  28767  xpinpreima  31391  xpinpreima2  31392  eulerpartgbij  31872  topdifinfeq  35083  rabimbieq  35989  rmydioph  40374  rmxdioph  40376  expdiophlem2  40382  expdioph  40383  alephiso3  40677  fsovrfovd  41129  k0004val0  41276  nzss  41440  hashnzfz  41443  fourierdlem90  43250  fourierdlem96  43256  fourierdlem97  43257  fourierdlem98  43258  fourierdlem99  43259  fourierdlem100  43260  fourierdlem109  43269  fourierdlem110  43270  fourierdlem112  43272  fourierdlem113  43273  sssmf  43784  dfodd6  44582  dfeven4  44583  dfeven2  44594  dfodd3  44595  dfeven3  44603  dfodd4  44604  dfodd5  44605