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

Theorem opabssxp 5778
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 482 . . 3 (((𝑥𝐴𝑦𝐵) ∧ 𝜑) → (𝑥𝐴𝑦𝐵))
21ssopab2i 5555 . 2 {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝜑)} ⊆ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐵)}
3 df-xp 5691 . 2 (𝐴 × 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐵)}
42, 3sseqtrri 4033 1 {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝜑)} ⊆ (𝐴 × 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wa 395  wcel 2108  wss 3951  {copab 5205   × cxp 5683
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-ss 3968  df-opab 5206  df-xp 5691
This theorem is referenced by:  brab2a  5779  dmoprabss  7537  ecopovsym  8859  ecopovtrn  8860  ecopover  8861  enqex  10962  lterpq  11010  ltrelpr  11038  enrex  11107  ltrelsr  11108  ltrelre  11174  ltrelxr  11322  rlimpm  15536  dvdszrcl  16295  prdsle  17507  prdsless  17508  sectfval  17795  sectss  17796  ltbval  22061  opsrle  22065  lmfval  23240  isphtpc  25026  bcthlem1  25358  bcthlem5  25362  lgsquadlem1  27424  lgsquadlem2  27425  lgsquadlem3  27426  ishlg  28610  perpln1  28718  perpln2  28719  isperp  28720  iscgra  28817  isinag  28846  isleag  28855  inftmrel  33187  isinftm  33188  fldextfld1  33700  fldextfld2  33701  metidval  33889  metidss  33890  faeval  34247  filnetlem2  36380  numiunnum  36471  areacirc  37720  lcvfbr  39021  cmtfvalN  39211  cvrfval  39269  dicssdvh  41188  aks6d1c1p1rcl  42109  pellexlem3  42842  pellexlem4  42843  pellexlem5  42844  pellex  42846  rfovcnvf1od  44017  fsovrfovd  44022
  Copyright terms: Public domain W3C validator