Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (Proof shortened by Mario Carneiro, 22-Dec-2016) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypothesis | bnj23.1 | |
|
Assertion | bnj23 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bnj23.1 | |
|
2 | sbcng | |
|
3 | 2 | elv | |
4 | 1 | eleq2i | |
5 | nfcv | |
|
6 | 5 | elrabsf | |
7 | 4 6 | bitri | |
8 | breq1 | |
|
9 | 8 | notbid | |
10 | 9 | rspccv | |
11 | 7 10 | syl5bir | |
12 | 11 | expdimp | |
13 | 3 12 | syl5bir | |
14 | 13 | con4d | |
15 | 14 | ralrimiva | |