Metamath Proof Explorer

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∈𝑸∧B∈𝑸∧A~𝑸B→A=B

Proof

Step Hyp Ref Expression
1 3simpa ⊢A∈𝑸∧B∈𝑸∧A~𝑸B→A∈𝑸∧B∈𝑸
2 elpqn ⊢B∈𝑸→B∈𝑵×𝑵
3 2 3ad2ant2 ⊢A∈𝑸∧B∈𝑸∧A~𝑸B→B∈𝑵×𝑵
4 nqereu ⊢B∈𝑵×𝑵→∃!x∈𝑸x~𝑸B
5 reurmo ⊢∃!x∈𝑸x~𝑸B→∃*x∈𝑸x~𝑸B
6 3 4 5 3syl ⊢A∈𝑸∧B∈𝑸∧A~𝑸B→∃*x∈𝑸x~𝑸B
7 df-rmo ⊢∃*x∈𝑸x~𝑸B↔∃*xx∈𝑸∧x~𝑸B
8 6 7 sylib ⊢A∈𝑸∧B∈𝑸∧A~𝑸B→∃*xx∈𝑸∧x~𝑸B
9 3simpb ⊢A∈𝑸∧B∈𝑸∧A~𝑸B→A∈𝑸∧A~𝑸B
10 simp2 ⊢A∈𝑸∧B∈𝑸∧A~𝑸B→B∈𝑸
11 enqer ⊢~𝑸Er𝑵×𝑵
12 11 a1i ⊢A∈𝑸∧B∈𝑸∧A~𝑸B→~𝑸Er𝑵×𝑵
13 12 3 erref ⊢A∈𝑸∧B∈𝑸∧A~𝑸B→B~𝑸B
14 10 13 jca ⊢A∈𝑸∧B∈𝑸∧A~𝑸B→B∈𝑸∧B~𝑸B
15 eleq1 ⊢x=A→x∈𝑸↔A∈𝑸
16 breq1 ⊢x=A→x~𝑸B↔A~𝑸B
17 15 16 anbi12d ⊢x=A→x∈𝑸∧x~𝑸B↔A∈𝑸∧A~𝑸B
18 eleq1 ⊢x=B→x∈𝑸↔B∈𝑸
19 breq1 ⊢x=B→x~𝑸B↔B~𝑸B
20 18 19 anbi12d ⊢x=B→x∈𝑸∧x~𝑸B↔B∈𝑸∧B~𝑸B
21 17 20 moi ⊢A∈𝑸∧B∈𝑸∧∃*xx∈𝑸∧x~𝑸B∧A∈𝑸∧A~𝑸B∧B∈𝑸∧B~𝑸B→A=B
22 1 8 9 14 21 syl112anc ⊢A∈𝑸∧B∈𝑸∧A~𝑸B→A=B