Description: Double restricted existential quantification. (Contributed by NM, 11-Nov-1995) Reduce dependencies on axioms. (Revised by Wolf Lammen, 10-Jan-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | r2ex | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | r2al | |
|
2 | 1 | r2exlem | |