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  4482  mptiniseg  5285  elovmporab  6292  supeq1  7333  supeq2  7336  supeq3  7337  cardcl  7533  isnumi  7534  cardval3ex  7537  carden2bex  7542  genpdflem  7881  genipv  7883  genpelxp  7885  addcomprg  7952  mulcomprg  7954  uzval  9940  ixxval  10316  fzval  10431  hashinfom  11240  hashennn  11242  ssenneg  11303  hashfibclem  11305  hashfibc  11306  shftfn  11612  bitsfval  12735  gcdval  12762  lcmval  12867  isprm  12913  odzval  13050  pceulem  13103  pceu  13104  pcval  13105  pczpre  13106  pcdiv  13111  ballotfilemi  13302  ballotfi  13341  cntzval  14154  cntzsnval  14157  lspval  14837  aspval  15125  psrass1filem  15182  psrmulvalfi  15193  istopon  15251  toponsspwpwg  15260  clsval  15349  neival  15381  cnpval  15436  blvalps  15626  blval  15627  limccl  15897  ellimc3apf  15898  eldvap  15920  sgmval  16264  vtxdgfifival  16749  clwwlknon  16887  clwwlk0on0  16889  eupth2fi  16937