Theorem rabbidv 2790

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 2789	1 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒})

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

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 2212

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1810  df-clab 2217  df-cleq 2223  df-ral 2514  df-rab 2518

This theorem is referenced by:  rabeqbidv  2796  difeq2  3318  seex  4434  mptiniseg  5233  elovmporab  6227  supeq1  7190  supeq2  7193  supeq3  7194  cardcl  7390  isnumi  7391  cardval3ex  7394  carden2bex  7399  genpdflem  7732  genipv  7734  genpelxp  7736  addcomprg  7803  mulcomprg  7805  uzval  9762  ixxval  10136  fzval  10250  hashinfom  11046  hashennn  11048  shftfn  11407  bitsfval  12526  gcdval  12553  lcmval  12658  isprm  12704  odzval  12837  pceulem  12890  pceu  12891  pcval  12892  pczpre  12893  pcdiv  12898  lspval  14428  istopon  14766  toponsspwpwg  14775  clsval  14864  neival  14896  cnpval  14951  blvalps  15141  blval  15142  limccl  15412  ellimc3apf  15413  eldvap  15435  sgmval  15736  vtxdgfifival  16171  clwwlknon  16309  clwwlk0on0  16311  eupth2fi  16359