Theorem rabbidva 2645

Description: Equivalent wff's yield equal restricted class abstractions (deduction form). (Contributed by NM, 28-Nov-2003.)

Hypothesis

Ref	Expression
rabbidva.1	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))

Assertion

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

Distinct variable group:   𝜑,𝑥

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

Proof of Theorem rabbidva

Step	Hyp	Ref	Expression
1		rabbidva.1	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))
2	1	ralrimiva 2479	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝜓 ↔ 𝜒))
3		rabbi 2582	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜓 ↔ 𝜒) ↔ {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒})
4	2, 3	sylib 121	1 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒})

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   = wceq 1314   ∈ wcel 1463  ∀wral 2390  {crab 2394

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-11 1467  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097

This theorem depends on definitions:  df-bi 116  df-tru 1317  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-ral 2395  df-rab 2399

This theorem is referenced by:  rabbidv  2646  rabeqbidva  2653  rabbi2dva  3250  rabxfrd  4350  onsucmin  4383  seinxp  4570  fniniseg2  5496  fnniniseg2  5497  f1oresrab  5539  dfinfre  8624  minmax  10893  xrminmax  10926  iooinsup  10938  gcdass  11549  lcmass  11612  bdbl  12492  xmetxpbl  12497