Theorem rabbidv 2810

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1402   ∈ wcel 2209  {crab 2532

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 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-ral 2533  df-rab 2537

This theorem is referenced by:  rabeqbidv  2816  difeq2  3341  seex  4478  mptiniseg  5280  elovmporab  6283  supeq1  7320  supeq2  7323  supeq3  7324  cardcl  7520  isnumi  7521  cardval3ex  7524  carden2bex  7529  genpdflem  7868  genipv  7870  genpelxp  7872  addcomprg  7939  mulcomprg  7941  uzval  9906  ixxval  10281  fzval  10396  hashinfom  11200  hashennn  11202  ssenneg  11263  hashfibclem  11265  hashfibc  11266  shftfn  11572  bitsfval  12692  gcdval  12719  lcmval  12824  isprm  12870  odzval  13003  pceulem  13056  pceu  13057  pcval  13058  pczpre  13059  pcdiv  13064  ballotfilemi  13226  ballotfi  13265  lspval  14710  aspval  14998  istopon  15097  toponsspwpwg  15106  clsval  15195  neival  15227  cnpval  15282  blvalps  15472  blval  15473  limccl  15743  ellimc3apf  15744  eldvap  15766  sgmval  16080  vtxdgfifival  16515  clwwlknon  16653  clwwlk0on0  16655  eupth2fi  16703