Description: At least two sets exist (or in terms of first-order logic, the universe of discourse has two or more objects). Note that we may not substitute the same variable for both x and y (as indicated by the distinct variable requirement), for otherwise we would contradict stdpc6 .
This theorem is proved directly from set theory axioms (no set theory definitions) and does not use ax-ext or ax-sep . See dtruALT for a shorter proof using these axioms.
The proof makes use of dummy variables z and w which do not appear in the final theorem. They must be distinct from each other and from x and y . In other words, if we were to substitute x for z throughout the proof, the proof would fail. (Contributed by NM, 7-Nov-2006) Avoid ax-13 . (Revised by Gino Giotto, 5-Sep-2023)
Ref | Expression | ||
---|---|---|---|
Assertion | dtru |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | el | ||
2 | ax-nul | ||
3 | sp | ||
4 | 2 3 | eximii | |
5 | exdistrv | ||
6 | 1 4 5 | mpbir2an | |
7 | ax9v2 | ||
8 | 7 | com12 | |
9 | 8 | con3dimp | |
10 | 9 | 2eximi | |
11 | equequ2 | ||
12 | 11 | notbid | |
13 | nfv | ||
14 | ax7v1 | ||
15 | 14 | con3d | |
16 | 13 15 | spimefv | |
17 | 12 16 | syl6bi | |
18 | nfv | ||
19 | ax7v1 | ||
20 | 19 | con3d | |
21 | 18 20 | spimefv | |
22 | 21 | a1d | |
23 | 17 22 | pm2.61i | |
24 | 23 | exlimivv | |
25 | 6 10 24 | mp2b | |
26 | exnal | ||
27 | 25 26 | mpbi |