Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > int0 | Structured version Visualization version GIF version |
Description: The intersection of the empty set is the universal class. Exercise 2 of [TakeutiZaring] p. 44. (Contributed by NM, 18-Aug-1993.) (Proof shortened by JJ, 26-Jul-2021.) |
Ref | Expression |
---|---|
int0 | ⊢ ∩ ∅ = V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ral0 4455 | . . . 4 ⊢ ∀𝑥 ∈ ∅ 𝑦 ∈ 𝑥 | |
2 | vex 3497 | . . . . 5 ⊢ 𝑦 ∈ V | |
3 | 2 | elint2 4875 | . . . 4 ⊢ (𝑦 ∈ ∩ ∅ ↔ ∀𝑥 ∈ ∅ 𝑦 ∈ 𝑥) |
4 | 1, 3 | mpbir 233 | . . 3 ⊢ 𝑦 ∈ ∩ ∅ |
5 | 4, 2 | 2th 266 | . 2 ⊢ (𝑦 ∈ ∩ ∅ ↔ 𝑦 ∈ V) |
6 | 5 | eqriv 2818 | 1 ⊢ ∩ ∅ = V |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1533 ∈ wcel 2110 ∀wral 3138 Vcvv 3494 ∅c0 4290 ∩ cint 4868 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2157 ax-12 2173 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ral 3143 df-v 3496 df-dif 3938 df-nul 4291 df-int 4869 |
This theorem is referenced by: unissint 4892 uniintsn 4905 rint0 4908 intex 5232 intnex 5233 oev2 8142 fiint 8789 elfi2 8872 fi0 8878 cardmin2 9421 00lsp 19747 cmpfi 22010 ptbasfi 22183 fbssint 22440 fclscmp 22632 rankeq1o 33627 bj-0int 34387 heibor1lem 35081 |
Copyright terms: Public domain | W3C validator |