Theorem rabbidv 2791

Description: Equivalent wff's yield equal restricted class abstractions (deduction form). (Contributed by NM, 10-Feb-1995.)

Hypothesis

Ref	Expression
rabbidv.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
rabbidv	⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒})

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem rabbidv

Step	Hyp	Ref	Expression
1		rabbidv.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	adantr 276	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))
3	2	rabbidva 2790	1 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒})

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1397   ∈ wcel 2202  {crab 2514

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-ral 2515  df-rab 2519

This theorem is referenced by:  rabeqbidv  2797  difeq2  3319  seex  4432  mptiniseg  5231  elovmporab  6222  supeq1  7185  supeq2  7188  supeq3  7189  cardcl  7385  isnumi  7386  cardval3ex  7389  carden2bex  7394  genpdflem  7727  genipv  7729  genpelxp  7731  addcomprg  7798  mulcomprg  7800  uzval  9757  ixxval  10131  fzval  10245  hashinfom  11041  hashennn  11043  shftfn  11386  bitsfval  12505  gcdval  12532  lcmval  12637  isprm  12683  odzval  12816  pceulem  12869  pceu  12870  pcval  12871  pczpre  12872  pcdiv  12877  lspval  14407  istopon  14740  toponsspwpwg  14749  clsval  14838  neival  14870  cnpval  14925  blvalps  15115  blval  15116  limccl  15386  ellimc3apf  15387  eldvap  15409  sgmval  15710  vtxdgfifival  16145  clwwlknon  16283  clwwlk0on0  16285  eupth2fi  16333