![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > equsexALT | Structured version Visualization version Unicode version |
Description: Alternate proof of equsex 2140. This proves the result directly, instead of as a corollary of equsal 2138 via equs4 2137. Note in particular that only existential quantifiers appear in the proof and that the only step requiring ax-13 2101 is ax6e 2104. This proof mimics that of equsal 2138 (in particular, note pm5.32i 647, exbii 1728, 19.41 2061, mpbiran 934 correspond respectively to pm5.74i 253, albii 1701, 19.23 2003, a1bi 343). (Contributed by BJ, 20-Aug-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
Ref | Expression |
---|---|
equsex.nf |
![]() ![]() ![]() ![]() |
equsex.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
equsexALT |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | equsex.1 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | pm5.32i 647 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | exbii 1728 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | ax6e 2104 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
5 | equsex.nf |
. . . 4
![]() ![]() ![]() ![]() | |
6 | 5 | 19.41 2061 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 4, 6 | mpbiran 934 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | 3, 7 | bitri 257 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1679 ax-4 1692 ax-5 1768 ax-6 1815 ax-7 1861 ax-10 1925 ax-12 1943 ax-13 2101 |
This theorem depends on definitions: df-bi 190 df-an 377 df-ex 1674 df-nf 1678 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |