Theorem opabssxp 5710

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

Step	Hyp	Ref	Expression
1		simpl 483	. . 3 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
2	1	ssopab2i 5492	. 2 ⊢ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)} ⊆ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}
3		df-xp 5624	. 2 ⊢ (𝐴 × 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}
4	2, 3	sseqtrri 3964	1 ⊢ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)} ⊆ (𝐴 × 𝐵)

Syntax hints:   ∧ wa 396   ∈ wcel 2119   ⊆ wss 3883  {copab 5134   × cxp 5616

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-ss 3900  df-opab 5135  df-xp 5624

This theorem is referenced by:  brab2a  5711  dmoprabss  7460  ecopovsym  8756  ecopovtrn  8757  ecopover  8758  enqex  10836  lterpq  10884  ltrelpr  10912  enrex  10981  ltrelsr  10982  ltrelre  11048  ltrelxr  11197  rlimpm  15453  dvdszrcl  16217  prdsle  17416  prdsless  17417  sectfval  17709  sectss  17710  ltbval  22019  opsrle  22023  lmfval  23215  isphtpc  24979  bcthlem1  25309  bcthlem5  25313  lgsquadlem1  27361  lgsquadlem2  27362  lgsquadlem3  27363  ishlg  28688  perpln1  28796  perpln2  28797  isperp  28798  iscgra  28895  isinag  28924  isleag  28933  inftmrel  33261  isinftm  33262  fldextfld1  33831  fldextfld2  33832  metidval  34074  metidss  34075  faeval  34430  filnetlem2  36607  numiunnum  36698  areacirc  38080  lcvfbr  39512  cmtfvalN  39702  cvrfval  39760  dicssdvh  41678  aks6d1c1p1rcl  42593  pellexlem3  43276  pellexlem4  43277  pellexlem5  43278  pellex  43280  rfovcnvf1od  44448  fsovrfovd  44453  sectfn  49519