Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  dvdszrcl Structured version   Visualization version   GIF version

Theorem dvdszrcl 15604
 Description: Reverse closure for the divisibility relation. (Contributed by Stefan O'Rear, 5-Sep-2015.)
Assertion
Ref Expression
dvdszrcl (𝑋𝑌 → (𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ))

Proof of Theorem dvdszrcl
Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-dvds 15600 . . 3 ∥ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ ∃𝑧 ∈ ℤ (𝑧 · 𝑥) = 𝑦)}
2 opabssxp 5641 . . 3 {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ ∃𝑧 ∈ ℤ (𝑧 · 𝑥) = 𝑦)} ⊆ (ℤ × ℤ)
31, 2eqsstri 4004 . 2 ∥ ⊆ (ℤ × ℤ)
43brel 5615 1 (𝑋𝑌 → (𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 396   = wceq 1530   ∈ wcel 2107  ∃wrex 3143   class class class wbr 5062  {copab 5124   × cxp 5551  (class class class)co 7151   · cmul 10534  ℤcz 11973   ∥ cdvds 15599 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2797  ax-sep 5199  ax-nul 5206  ax-pr 5325 This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2804  df-cleq 2818  df-clel 2897  df-nfc 2967  df-ral 3147  df-rex 3148  df-rab 3151  df-v 3501  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4470  df-sn 4564  df-pr 4566  df-op 4570  df-br 5063  df-opab 5125  df-xp 5559  df-dvds 15600 This theorem is referenced by:  dvdsmod0  15605  p1modz1  15606  dvdsmodexp  15607  dvdsaddre2b  15649  dvdsabseq  15655  divconjdvds  15657  evenelz  15677  4dvdseven  15716  dfgcd2  15886  dvdsmulgcd  15897  dvdsnprmd  16026  oddvdsi  18598  odmulg  18605  gexdvdsi  18630  dvdszzq  30446  dvdschrmulg  30774  nzss  40516  nzin  40517
 Copyright terms: Public domain W3C validator