Theorem rabbiia 3472

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

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

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 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-sb 2070  df-clab 2800  df-cleq 2814  df-rab 3147

This theorem is referenced by:  rabbii  3473  fninfp  6936  fndifnfp  6938  nlimon  7566  dfom2  7582  rankval2  9247  ioopos  12814  prmreclem4  16255  acsfn1  16932  acsfn2  16934  logtayl  25243  ftalem3  25652  ppiub  25780  isuvtx  27177  vtxdginducedm1  27325  finsumvtxdg2size  27332  rgrusgrprc  27371  clwwlknclwwlkdif  27757  numclwwlkqhash  28154  ubthlem1  28647  xpinpreima  31149  xpinpreima2  31150  eulerpartgbij  31630  topdifinfeq  34634  rabimbieq  35528  rmydioph  39660  rmxdioph  39662  expdiophlem2  39668  expdioph  39669  alephiso3  39967  fsovrfovd  40404  k0004val0  40553  nzss  40698  hashnzfz  40701  fourierdlem90  42530  fourierdlem96  42536  fourierdlem97  42537  fourierdlem98  42538  fourierdlem99  42539  fourierdlem100  42540  fourierdlem109  42549  fourierdlem110  42550  fourierdlem112  42552  fourierdlem113  42553  sssmf  43064  dfodd6  43851  dfeven4  43852  dfeven2  43863  dfodd3  43864  dfeven3  43872  dfodd4  43873  dfodd5  43874