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

Theorem opabssxp 5636
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 483 . . 3 (((𝑥𝐴𝑦𝐵) ∧ 𝜑) → (𝑥𝐴𝑦𝐵))
21ssopab2i 5428 . 2 {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝜑)} ⊆ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐵)}
3 df-xp 5554 . 2 (𝐴 × 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐵)}
42, 3sseqtrri 4001 1 {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝜑)} ⊆ (𝐴 × 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wa 396  wcel 2105  wss 3933  {copab 5119   × cxp 5546
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-in 3940  df-ss 3949  df-opab 5120  df-xp 5554
This theorem is referenced by:  brab2a  5637  dmoprabss  7245  ecopovsym  8388  ecopovtrn  8389  ecopover  8390  enqex  10332  lterpq  10380  ltrelpr  10408  enrex  10477  ltrelsr  10478  ltrelre  10544  ltrelxr  10690  rlimpm  14845  dvdszrcl  15600  prdsle  16723  prdsless  16724  sectfval  17009  sectss  17010  ltbval  20180  opsrle  20184  lmfval  21768  isphtpc  23525  bcthlem1  23854  bcthlem5  23858  lgsquadlem1  25883  lgsquadlem2  25884  lgsquadlem3  25885  ishlg  26315  perpln1  26423  perpln2  26424  isperp  26425  iscgra  26522  isinag  26551  isleag  26560  inftmrel  30736  isinftm  30737  fldextfld1  30938  fldextfld2  30939  metidval  31029  metidss  31030  faeval  31404  filnetlem2  33624  areacirc  34868  lcvfbr  36036  cmtfvalN  36226  cvrfval  36284  dicssdvh  38202  pellexlem3  39306  pellexlem4  39307  pellexlem5  39308  pellex  39310  rfovcnvf1od  40228  fsovrfovd  40233
  Copyright terms: Public domain W3C validator