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

This proof depends on syntax axioms:   → wi 4   ↔ wb 105   = wceq 1402   ∈ wcel 2209  {crab 2532

This proof depends on 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 proof 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 used by:  rabeqbidv  2816  difeq2  3341  seex  4480  mptiniseg  5282  elovmporab  6289  supeq1  7326  supeq2  7329  supeq3  7330  cardcl  7526  isnumi  7527  cardval3ex  7530  carden2bex  7535  genpdflem  7874  genipv  7876  genpelxp  7878  addcomprg  7945  mulcomprg  7947  uzval  9925  ixxval  10300  fzval  10415  hashinfom  11219  hashennn  11221  ssenneg  11282  hashfibclem  11284  hashfibc  11285  shftfn  11591  bitsfval  12711  gcdval  12738  lcmval  12843  isprm  12889  odzval  13022  pceulem  13075  pceu  13076  pcval  13077  pczpre  13078  pcdiv  13083  ballotfilemi  13245  ballotfi  13284  lspval  14729  aspval  15017  istopon  15116  toponsspwpwg  15125  clsval  15214  neival  15246  cnpval  15301  blvalps  15491  blval  15492  limccl  15762  ellimc3apf  15763  eldvap  15785  sgmval  16103  vtxdgfifival  16544  clwwlknon  16682  clwwlk0on0  16684  eupth2fi  16732