Theorem 1nq 7340

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 7289	. . . 4 ⊢ 1o ∈ N
2		opelxpi 4652	. . . 4 ⊢ ((1o ∈ N ∧ 1o ∈ N) → ⟨1o, 1o⟩ ∈ (N × N))
3	1, 1, 2	mp2an 426	. . 3 ⊢ ⟨1o, 1o⟩ ∈ (N × N)
4		enqex 7334	. . . 4 ⊢ ~Q ∈ V
5	4	ecelqsi 6579	. . 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 7325	. 2 ⊢ 1Q = [⟨1o, 1o⟩] ~Q
8		df-nqqs 7322	. 2 ⊢ Q = ((N × N) / ~Q )
9	6, 7, 8	3eltr4i 2257	1 ⊢ 1Q ∈ Q

Syntax hints:   ∈ wcel 2146  ⟨cop 3592   × cxp 4618  1_oc1o 6400  [cec 6523   / cqs 6524  Ncnpi 7246   ~_Q ceq 7253  Qcnq 7254  1_Qc1q 7255

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 614  ax-in2 615  ax-io 709  ax-5 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-13 2148  ax-14 2149  ax-ext 2157  ax-sep 4116  ax-nul 4124  ax-pow 4169  ax-pr 4203  ax-un 4427  ax-iinf 4581

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1459  df-sb 1761  df-eu 2027  df-mo 2028  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-ne 2346  df-ral 2458  df-rex 2459  df-v 2737  df-dif 3129  df-un 3131  df-in 3133  df-ss 3140  df-nul 3421  df-pw 3574  df-sn 3595  df-pr 3596  df-op 3598  df-uni 3806  df-int 3841  df-br 3999  df-opab 4060  df-suc 4365  df-iom 4584  df-xp 4626  df-cnv 4628  df-dm 4630  df-rn 4631  df-res 4632  df-ima 4633  df-1o 6407  df-ec 6527  df-qs 6531  df-ni 7278  df-enq 7321  df-nqqs 7322  df-1nqqs 7325

This theorem is referenced by:  recmulnqg  7365  rec1nq  7369  ltaddnq  7381  halfnqq  7384  addnqprllem  7501  addnqprulem  7502  1pr  7528  addnqpr1  7536  appdivnq  7537  1idprl  7564  1idpru  7565  recexprlemm  7598  recexprlem1ssl  7607  recexprlem1ssu  7608  cauappcvgprlemm  7619  caucvgprlemm  7642  caucvgprprlemmu  7669  suplocexprlemmu  7692