Theorem 1nq 7521

Description: The positive fraction 'one'. (Contributed by NM, 29-Oct-1995.)

Assertion

Ref	Expression
1nq	⊢ 1Q ∈ Q

Proof of Theorem 1nq

Step	Hyp	Ref	Expression
1		1pi 7470	. . . 4 ⊢ 1o ∈ N
2		opelxpi 4728	. . . 4 ⊢ ((1o ∈ N ∧ 1o ∈ N) → ⟨1o, 1o⟩ ∈ (N × N))
3	1, 1, 2	mp2an 426	. . 3 ⊢ ⟨1o, 1o⟩ ∈ (N × N)
4		enqex 7515	. . . 4 ⊢ ~Q ∈ V
5	4	ecelqsi 6706	. . 3 ⊢ (⟨1o, 1o⟩ ∈ (N × N) → [⟨1o, 1o⟩] ~Q ∈ ((N × N) / ~Q ))
6	3, 5	ax-mp 5	. 2 ⊢ [⟨1o, 1o⟩] ~Q ∈ ((N × N) / ~Q )
7		df-1nqqs 7506	. 2 ⊢ 1Q = [⟨1o, 1o⟩] ~Q
8		df-nqqs 7503	. 2 ⊢ Q = ((N × N) / ~Q )
9	6, 7, 8	3eltr4i 2291	1 ⊢ 1Q ∈ Q

Syntax hints:   ∈ wcel 2180  ⟨cop 3649   × cxp 4694  1_oc1o 6525  [cec 6648   / cqs 6649  Ncnpi 7427   ~_Q ceq 7434  Qcnq 7435  1_Qc1q 7436

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 617  ax-in2 618  ax-io 713  ax-5 1473  ax-7 1474  ax-gen 1475  ax-ie1 1519  ax-ie2 1520  ax-8 1530  ax-10 1531  ax-11 1532  ax-i12 1533  ax-bndl 1535  ax-4 1536  ax-17 1552  ax-i9 1556  ax-ial 1560  ax-i5r 1561  ax-13 2182  ax-14 2183  ax-ext 2191  ax-sep 4181  ax-nul 4189  ax-pow 4237  ax-pr 4272  ax-un 4501  ax-iinf 4657

This theorem depends on definitions:  df-bi 117  df-3an 985  df-tru 1378  df-nf 1487  df-sb 1789  df-eu 2060  df-mo 2061  df-clab 2196  df-cleq 2202  df-clel 2205  df-nfc 2341  df-ne 2381  df-ral 2493  df-rex 2494  df-v 2781  df-dif 3179  df-un 3181  df-in 3183  df-ss 3190  df-nul 3472  df-pw 3631  df-sn 3652  df-pr 3653  df-op 3655  df-uni 3868  df-int 3903  df-br 4063  df-opab 4125  df-suc 4439  df-iom 4660  df-xp 4702  df-cnv 4704  df-dm 4706  df-rn 4707  df-res 4708  df-ima 4709  df-1o 6532  df-ec 6652  df-qs 6656  df-ni 7459  df-enq 7502  df-nqqs 7503  df-1nqqs 7506

This theorem is referenced by:  recmulnqg  7546  rec1nq  7550  ltaddnq  7562  halfnqq  7565  addnqprllem  7682  addnqprulem  7683  1pr  7709  addnqpr1  7717  appdivnq  7718  1idprl  7745  1idpru  7746  recexprlemm  7779  recexprlem1ssl  7788  recexprlem1ssu  7789  cauappcvgprlemm  7800  caucvgprlemm  7823  caucvgprprlemmu  7850  suplocexprlemmu  7873