Theorem enqeq

Description: Corollary of nqereu : if two fractions are both reduced and equivalent, then they are equal. (Contributed by Mario Carneiro, 6-May-2013) (New usage is discouraged.)

	Ref	Expression
Assertion	enqeq	|- ( ( A e. Q. /\ B e. Q. /\ A ~Q B ) -> A = B )

Proof

Step	Hyp	Ref	Expression
1		3simpa	|- ( ( A e. Q. /\ B e. Q. /\ A ~Q B ) -> ( A e. Q. /\ B e. Q. ) )
2		elpqn	|- ( B e. Q. -> B e. ( N. X. N. ) )
3	2	3ad2ant2	|- ( ( A e. Q. /\ B e. Q. /\ A ~Q B ) -> B e. ( N. X. N. ) )
4		nqereu	|- ( B e. ( N. X. N. ) -> E! x e. Q. x ~Q B )
5		reurmo	|- ( E! x e. Q. x ~Q B -> E* x e. Q. x ~Q B )
6	3 4 5	3syl	|- ( ( A e. Q. /\ B e. Q. /\ A ~Q B ) -> E* x e. Q. x ~Q B )
7		df-rmo	|- ( E* x e. Q. x ~Q B <-> E* x ( x e. Q. /\ x ~Q B ) )
8	6 7	sylib	|- ( ( A e. Q. /\ B e. Q. /\ A ~Q B ) -> E* x ( x e. Q. /\ x ~Q B ) )
9		3simpb	|- ( ( A e. Q. /\ B e. Q. /\ A ~Q B ) -> ( A e. Q. /\ A ~Q B ) )
10		simp2	|- ( ( A e. Q. /\ B e. Q. /\ A ~Q B ) -> B e. Q. )
11		enqer	|- ~Q Er ( N. X. N. )
12	11	a1i	|- ( ( A e. Q. /\ B e. Q. /\ A ~Q B ) -> ~Q Er ( N. X. N. ) )
13	12 3	erref	|- ( ( A e. Q. /\ B e. Q. /\ A ~Q B ) -> B ~Q B )
14	10 13	jca	|- ( ( A e. Q. /\ B e. Q. /\ A ~Q B ) -> ( B e. Q. /\ B ~Q B ) )
15		eleq1	|- ( x = A -> ( x e. Q. <-> A e. Q. ) )
16		breq1	|- ( x = A -> ( x ~Q B <-> A ~Q B ) )
17	15 16	anbi12d	|- ( x = A -> ( ( x e. Q. /\ x ~Q B ) <-> ( A e. Q. /\ A ~Q B ) ) )
18		eleq1	|- ( x = B -> ( x e. Q. <-> B e. Q. ) )
19		breq1	|- ( x = B -> ( x ~Q B <-> B ~Q B ) )
20	18 19	anbi12d	|- ( x = B -> ( ( x e. Q. /\ x ~Q B ) <-> ( B e. Q. /\ B ~Q B ) ) )
21	17 20	moi	|- ( ( ( A e. Q. /\ B e. Q. ) /\ E* x ( x e. Q. /\ x ~Q B ) /\ ( ( A e. Q. /\ A ~Q B ) /\ ( B e. Q. /\ B ~Q B ) ) ) -> A = B )
22	1 8 9 14 21	syl112anc	|- ( ( A e. Q. /\ B e. Q. /\ A ~Q B ) -> A = B )