Description: Alternate proof of reex . (Contributed by NM, 30-Jul-2004) (Revised by Mario Carneiro, 23-Aug-2014) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | reexALT | |- RR e. _V |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nnexALT | |- NN e. _V |
|
| 2 | qexALT | |- QQ e. _V |
|
| 3 | 1 2 | rpnnen1 | |- RR ~<_ ( QQ ^m NN ) |
| 4 | reldom | |- Rel ~<_ |
|
| 5 | 4 | brrelex1i | |- ( RR ~<_ ( QQ ^m NN ) -> RR e. _V ) |
| 6 | 3 5 | ax-mp | |- RR e. _V |