![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > r2ex | Structured version Unicode version |
Description: Double restricted existential quantification. (Contributed by NM, 11-Nov-1995.) |
Ref | Expression |
---|---|
r2ex |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfcv 2614 |
. 2
![]() ![]() ![]() ![]() | |
2 | 1 | r2exf 2870 |
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 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1954 ax-ext 2431 |
This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-ex 1588 df-nf 1591 df-sb 1703 df-cleq 2444 df-clel 2447 df-nfc 2602 df-rex 2802 |
This theorem is referenced by: reean 2987 rnoprab2 6279 elrnmpt2res 6309 oeeu 7147 omxpenlem 7517 axcnre 9437 pmtrrn2 16080 fsumvma 22680 usgrarnedg 23450 spanuni 25094 5oalem7 25210 3oalem3 25214 elfuns 28085 ellines 28322 hash2prv 30369 hash2sspr 30370 dalem20 33656 diblsmopel 35135 |
Copyright terms: Public domain | W3C validator |