New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > eluni | GIF version |
Description: Membership in class union. (Contributed by NM, 22-May-1994.) |
Ref | Expression |
---|---|
eluni | ⊢ (A ∈ ∪B ↔ ∃x(A ∈ x ∧ x ∈ B)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elex 2867 | . 2 ⊢ (A ∈ ∪B → A ∈ V) | |
2 | elex 2867 | . . . 4 ⊢ (A ∈ x → A ∈ V) | |
3 | 2 | adantr 451 | . . 3 ⊢ ((A ∈ x ∧ x ∈ B) → A ∈ V) |
4 | 3 | exlimiv 1634 | . 2 ⊢ (∃x(A ∈ x ∧ x ∈ B) → A ∈ V) |
5 | eleq1 2413 | . . . . 5 ⊢ (y = A → (y ∈ x ↔ A ∈ x)) | |
6 | 5 | anbi1d 685 | . . . 4 ⊢ (y = A → ((y ∈ x ∧ x ∈ B) ↔ (A ∈ x ∧ x ∈ B))) |
7 | 6 | exbidv 1626 | . . 3 ⊢ (y = A → (∃x(y ∈ x ∧ x ∈ B) ↔ ∃x(A ∈ x ∧ x ∈ B))) |
8 | df-uni 3892 | . . 3 ⊢ ∪B = {y ∣ ∃x(y ∈ x ∧ x ∈ B)} | |
9 | 7, 8 | elab2g 2987 | . 2 ⊢ (A ∈ V → (A ∈ ∪B ↔ ∃x(A ∈ x ∧ x ∈ B))) |
10 | 1, 4, 9 | pm5.21nii 342 | 1 ⊢ (A ∈ ∪B ↔ ∃x(A ∈ x ∧ x ∈ B)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 176 ∧ wa 358 ∃wex 1541 = wceq 1642 ∈ wcel 1710 Vcvv 2859 ∪cuni 3891 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1546 ax-5 1557 ax-17 1616 ax-9 1654 ax-8 1675 ax-6 1729 ax-7 1734 ax-11 1746 ax-12 1925 ax-ext 2334 |
This theorem depends on definitions: df-bi 177 df-or 359 df-an 360 df-tru 1319 df-ex 1542 df-nf 1545 df-sb 1649 df-clab 2340 df-cleq 2346 df-clel 2349 df-nfc 2478 df-v 2861 df-uni 3892 |
This theorem is referenced by: eluni2 3895 elunii 3896 eluniab 3903 unipr 3905 uniun 3910 uniin 3911 uniss 3912 unissb 3921 unipw 4117 eluni1g 4172 unipw1 4325 nnadjoinlem1 4519 dmuni 4914 rnuni 5038 fununi 5160 funiunfv 5467 pw1fnex 5852 tcfnex 6244 |
Copyright terms: Public domain | W3C validator |