Description: Interchange class substitution and restricted existential quantifier. (Contributed by NM, 1-Mar-2008) (Proof shortened by Mario Carneiro, 13-Oct-2016) (Revised by NM, 18-Aug-2018) (Proof shortened by JJ, 7-Jul-2021)
Ref | Expression | ||
---|---|---|---|
Assertion | sbcrext | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sbcex | |
|
2 | 1 | a1i | |
3 | nfnfc1 | |
|
4 | id | |
|
5 | nfcvd | |
|
6 | 4 5 | nfeld | |
7 | sbcex | |
|
8 | 7 | 2a1i | |
9 | 3 6 8 | rexlimd2 | |
10 | sbcng | |
|
11 | 10 | adantl | |
12 | sbcralt | |
|
13 | 12 | ancoms | |
14 | 3 6 | nfan1 | |
15 | sbcng | |
|
16 | 15 | adantl | |
17 | 14 16 | ralbid | |
18 | 13 17 | bitrd | |
19 | 18 | notbid | |
20 | 11 19 | bitrd | |
21 | dfrex2 | |
|
22 | 21 | sbcbii | |
23 | dfrex2 | |
|
24 | 20 22 23 | 3bitr4g | |
25 | 24 | ex | |
26 | 2 9 25 | pm5.21ndd | |