ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  rabid2 GIF version

Theorem rabid2 2536
Description: An "identity" law for restricted class abstraction. (Contributed by NM, 9-Oct-2003.) (Proof shortened by Andrew Salmon, 30-May-2011.)
Assertion
Ref Expression
rabid2 (𝐴 = {𝑥𝐴𝜑} ↔ ∀𝑥𝐴 𝜑)
Distinct variable group:   𝑥,𝐴
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem rabid2
StepHypRef Expression
1 abeq2 2191 . . 3 (𝐴 = {𝑥 ∣ (𝑥𝐴𝜑)} ↔ ∀𝑥(𝑥𝐴 ↔ (𝑥𝐴𝜑)))
2 pm4.71 381 . . . 4 ((𝑥𝐴𝜑) ↔ (𝑥𝐴 ↔ (𝑥𝐴𝜑)))
32albii 1400 . . 3 (∀𝑥(𝑥𝐴𝜑) ↔ ∀𝑥(𝑥𝐴 ↔ (𝑥𝐴𝜑)))
41, 3bitr4i 185 . 2 (𝐴 = {𝑥 ∣ (𝑥𝐴𝜑)} ↔ ∀𝑥(𝑥𝐴𝜑))
5 df-rab 2362 . . 3 {𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
65eqeq2i 2093 . 2 (𝐴 = {𝑥𝐴𝜑} ↔ 𝐴 = {𝑥 ∣ (𝑥𝐴𝜑)})
7 df-ral 2358 . 2 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
84, 6, 73bitr4i 210 1 (𝐴 = {𝑥𝐴𝜑} ↔ ∀𝑥𝐴 𝜑)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wb 103  wal 1283   = wceq 1285  wcel 1434  {cab 2069  wral 2353  {crab 2357
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-11 1438  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065
This theorem depends on definitions:  df-bi 115  df-nf 1391  df-sb 1688  df-clab 2070  df-cleq 2076  df-clel 2079  df-ral 2358  df-rab 2362
This theorem is referenced by:  rabxmdc  3297  rabrsndc  3484  class2seteq  3963  dmmptg  4881  fneqeql  5351  fmpt  5393  acexmidlemph  5583  inffiexmid  6548  ssfirab  6567  ioomax  9260  iccmax  9261  dfphi2  10975  phiprmpw  10977  unennn  10989  znnen  10990
  Copyright terms: Public domain W3C validator