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

Theorem opabssxp 5102
Description: An abstraction relation is a subset of a related Cartesian product. (Contributed by NM, 16-Jul-1995.)
Assertion
Ref Expression
opabssxp {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝜑)} ⊆ (𝐴 × 𝐵)
Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦)

Proof of Theorem opabssxp
StepHypRef Expression
1 simpl 471 . . 3 (((𝑥𝐴𝑦𝐵) ∧ 𝜑) → (𝑥𝐴𝑦𝐵))
21ssopab2i 4914 . 2 {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝜑)} ⊆ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐵)}
3 df-xp 5030 . 2 (𝐴 × 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐵)}
42, 3sseqtr4i 3596 1 {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝜑)} ⊆ (𝐴 × 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wa 382  wcel 1975  wss 3535  {copab 4632   × cxp 5022
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-clab 2592  df-cleq 2598  df-clel 2601  df-nfc 2735  df-in 3542  df-ss 3549  df-opab 4634  df-xp 5030
This theorem is referenced by:  brab2ga  5103  dmoprabss  6614  ecopovsym  7709  ecopovtrn  7710  ecopover  7711  ecopoverOLD  7712  enqex  9596  lterpq  9644  ltrelpr  9672  enrex  9740  ltrelsr  9741  ltrelre  9807  ltrelxr  9946  rlimpm  14021  dvdszrcl  14768  prdsle  15887  prdsless  15888  sectfval  16176  sectss  16177  ltbval  19234  opsrle  19238  lmfval  20784  isphtpc  22528  bcthlem1  22842  bcthlem5  22846  lgsquadlem1  24818  lgsquadlem2  24819  lgsquadlem3  24820  ishlg  25211  perpln1  25319  perpln2  25320  isperp  25321  iscgra  25415  isinag  25443  isleag  25447  inftmrel  28867  isinftm  28868  metidval  29063  metidss  29064  faeval  29438  filnetlem2  31346  areacirc  32474  lcvfbr  33124  cmtfvalN  33314  cvrfval  33372  dicssdvh  35292  pellexlem3  36212  pellexlem4  36213  pellexlem5  36214  pellex  36216  rfovcnvf1od  37117  fsovrfovd  37122
  Copyright terms: Public domain W3C validator