Theorem rabbidv 2789

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1395   ∈ wcel 2200  {crab 2512

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-ral 2513  df-rab 2517

This theorem is referenced by:  rabeqbidv  2795  difeq2  3317  seex  4430  mptiniseg  5229  elovmporab  6217  supeq1  7179  supeq2  7182  supeq3  7183  cardcl  7379  isnumi  7380  cardval3ex  7383  carden2bex  7388  genpdflem  7720  genipv  7722  genpelxp  7724  addcomprg  7791  mulcomprg  7793  uzval  9750  ixxval  10124  fzval  10238  hashinfom  11033  hashennn  11035  shftfn  11378  bitsfval  12496  gcdval  12523  lcmval  12628  isprm  12674  odzval  12807  pceulem  12860  pceu  12861  pcval  12862  pczpre  12863  pcdiv  12868  lspval  14397  istopon  14730  toponsspwpwg  14739  clsval  14828  neival  14860  cnpval  14915  blvalps  15105  blval  15106  limccl  15376  ellimc3apf  15377  eldvap  15399  sgmval  15700  vtxdgfifival  16102  clwwlknon  16238  clwwlk0on0  16240