rexim - New Foundations Explorer

	New Foundations Explorer		< Previous Next > Nearby theorems
Mirrors > Home > NFE Home > Th. List > rexim		Unicode version

Theorem rexim 2718

Description: Theorem 19.22 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 22-Nov-1994.) (Proof shortened by Andrew Salmon, 30-May-2011.)

**Assertion**
Ref	Expression
rexim

**Proof of Theorem rexim**
Step	Hyp	Ref	Expression
1		con3 126	. . . 4
2	1	ral2imi 2690	. . 3
3	2	con3d 125	. 2
4		dfrex2 2627	. 2
5		dfrex2 2627	. 2
6	3, 4, 5	3imtr4g 261	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wral 2614

wrex 2615

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1546 ax-5 1557

This theorem depends on definitions: df-bi 177 df-an 360 df-ex 1542 df-ral 2619 df-rex 2620

This theorem is referenced by: reximia 2719 reximdai 2722 r19.29 2754 reupick2 3541 ss2iun 3984

W3C validator