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

Theorem eluni 3624
 Description: Membership in class union. (Contributed by NM, 22-May-1994.)
Assertion
Ref Expression
eluni (𝐴 𝐵 ↔ ∃𝑥(𝐴𝑥𝑥𝐵))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem eluni
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 elex 2618 . 2 (𝐴 𝐵𝐴 ∈ V)
2 elex 2618 . . . 4 (𝐴𝑥𝐴 ∈ V)
32adantr 270 . . 3 ((𝐴𝑥𝑥𝐵) → 𝐴 ∈ V)
43exlimiv 1530 . 2 (∃𝑥(𝐴𝑥𝑥𝐵) → 𝐴 ∈ V)
5 eleq1 2145 . . . . 5 (𝑦 = 𝐴 → (𝑦𝑥𝐴𝑥))
65anbi1d 453 . . . 4 (𝑦 = 𝐴 → ((𝑦𝑥𝑥𝐵) ↔ (𝐴𝑥𝑥𝐵)))
76exbidv 1748 . . 3 (𝑦 = 𝐴 → (∃𝑥(𝑦𝑥𝑥𝐵) ↔ ∃𝑥(𝐴𝑥𝑥𝐵)))
8 df-uni 3622 . . 3 𝐵 = {𝑦 ∣ ∃𝑥(𝑦𝑥𝑥𝐵)}
97, 8elab2g 2748 . 2 (𝐴 ∈ V → (𝐴 𝐵 ↔ ∃𝑥(𝐴𝑥𝑥𝐵)))
101, 4, 9pm5.21nii 653 1 (𝐴 𝐵 ↔ ∃𝑥(𝐴𝑥𝑥𝐵))
 Colors of variables: wff set class Syntax hints:   ∧ wa 102   ↔ wb 103   = wceq 1285  ∃wex 1422   ∈ wcel 1434  Vcvv 2609  ∪ cuni 3621 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-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  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-tru 1288  df-nf 1391  df-sb 1688  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-v 2611  df-uni 3622 This theorem is referenced by:  eluni2  3625  elunii  3626  eluniab  3633  uniun  3640  uniin  3641  uniss  3642  unissb  3651  dftr2  3897  unidif0  3961  unipw  4000  uniex2  4219  uniuni  4229  limom  4382  dmuni  4593  fununi  5018  nfvres  5258  elunirn  5457  tfrlem7  5986  tfrexlem  6003  tfrcldm  6032  bj-uniex2  10957
 Copyright terms: Public domain W3C validator