Theorem rabbidv 2768

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1375   ∈ wcel 2180  {crab 2492

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 1473  ax-7 1474  ax-gen 1475  ax-ie1 1519  ax-ie2 1520  ax-8 1530  ax-11 1532  ax-4 1536  ax-17 1552  ax-i9 1556  ax-ial 1560  ax-i5r 1561  ax-ext 2191

This theorem depends on definitions:  df-bi 117  df-tru 1378  df-nf 1487  df-sb 1789  df-clab 2196  df-cleq 2202  df-ral 2493  df-rab 2497

This theorem is referenced by:  rabeqbidv  2774  difeq2  3296  seex  4403  mptiniseg  5199  elovmporab  6176  supeq1  7121  supeq2  7124  supeq3  7125  cardcl  7321  isnumi  7322  cardval3ex  7325  carden2bex  7330  genpdflem  7662  genipv  7664  genpelxp  7666  addcomprg  7733  mulcomprg  7735  uzval  9692  ixxval  10060  fzval  10174  hashinfom  10967  hashennn  10969  shftfn  11301  bitsfval  12419  gcdval  12446  lcmval  12551  isprm  12597  odzval  12730  pceulem  12783  pceu  12784  pcval  12785  pczpre  12786  pcdiv  12791  lspval  14319  istopon  14652  toponsspwpwg  14661  clsval  14750  neival  14782  cnpval  14837  blvalps  15027  blval  15028  limccl  15298  ellimc3apf  15299  eldvap  15321  sgmval  15622