Theorem gtnqex 7516

Description: The class of rationals greater than a given rational is a set. (Contributed by Jim Kingdon, 13-Dec-2019.)

Assertion

Ref	Expression
gtnqex	⊢ {𝑥 ∣ 𝐴 <Q 𝑥} ∈ V

Proof of Theorem gtnqex

Step	Hyp	Ref	Expression
1		nqex 7329	. 2 ⊢ Q ∈ V
2		ltrelnq 7331	. . . . 5 ⊢ <Q ⊆ (Q × Q)
3	2	brel 4664	. . . 4 ⊢ (𝐴 <Q 𝑥 → (𝐴 ∈ Q ∧ 𝑥 ∈ Q))
4	3	simprd 113	. . 3 ⊢ (𝐴 <Q 𝑥 → 𝑥 ∈ Q)
5	4	abssi 3223	. 2 ⊢ {𝑥 ∣ 𝐴 <Q 𝑥} ⊆ Q
6	1, 5	ssexi 4128	1 ⊢ {𝑥 ∣ 𝐴 <Q 𝑥} ∈ V

Syntax hints:   ∈ wcel 2142  {cab 2157  Vcvv 2731   class class class wbr 3990  Qcnq 7246   <_Q cltq 7251

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 610  ax-in2 611  ax-io 705  ax-5 1441  ax-7 1442  ax-gen 1443  ax-ie1 1487  ax-ie2 1488  ax-8 1498  ax-10 1499  ax-11 1500  ax-i12 1501  ax-bndl 1503  ax-4 1504  ax-17 1520  ax-i9 1524  ax-ial 1528  ax-i5r 1529  ax-13 2144  ax-14 2145  ax-ext 2153  ax-coll 4105  ax-sep 4108  ax-pow 4161  ax-pr 4195  ax-un 4419  ax-iinf 4573

This theorem depends on definitions:  df-bi 116  df-3an 976  df-tru 1352  df-nf 1455  df-sb 1757  df-eu 2023  df-mo 2024  df-clab 2158  df-cleq 2164  df-clel 2167  df-nfc 2302  df-ral 2454  df-rex 2455  df-reu 2456  df-rab 2458  df-v 2733  df-sbc 2957  df-csb 3051  df-dif 3124  df-un 3126  df-in 3128  df-ss 3135  df-pw 3569  df-sn 3590  df-pr 3591  df-op 3593  df-uni 3798  df-int 3833  df-iun 3876  df-br 3991  df-opab 4052  df-mpt 4053  df-id 4279  df-iom 4576  df-xp 4618  df-rel 4619  df-cnv 4620  df-co 4621  df-dm 4622  df-rn 4623  df-res 4624  df-ima 4625  df-iota 5162  df-fun 5202  df-fn 5203  df-f 5204  df-f1 5205  df-fo 5206  df-f1o 5207  df-fv 5208  df-qs 6523  df-ni 7270  df-nqqs 7314  df-ltnqqs 7319

This theorem is referenced by:  nqprl  7517  nqpru  7518  1prl  7521  1pru  7522  addnqprlemrl  7523  addnqprlemru  7524  addnqprlemfl  7525  addnqprlemfu  7526  mulnqprlemrl  7539  mulnqprlemru  7540  mulnqprlemfl  7541  mulnqprlemfu  7542  ltnqpr  7559  ltnqpri  7560  archpr  7609  cauappcvgprlemladdfu  7620  cauappcvgprlemladdfl  7621  cauappcvgprlem2  7626  caucvgprlemladdfu  7643  caucvgprlem2  7646  caucvgprprlemopu  7665  suplocexprlemloc  7687