Theorem opabssxp 5717

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 5499	. 2 ⊢ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)} ⊆ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}
3		df-xp 5631	. 2 ⊢ (𝐴 × 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}
4	2, 3	sseqtrri 3971	1 ⊢ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)} ⊆ (𝐴 × 𝐵)

Syntax hints:   ∧ wa 396   ∈ wcel 2119   ⊆ wss 3890  {copab 5141   × cxp 5623

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 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-ss 3907  df-opab 5142  df-xp 5631

This theorem is referenced by:  brab2a  5718  dmoprabss  7467  ecopovsym  8763  ecopovtrn  8764  ecopover  8765  enqex  10843  lterpq  10891  ltrelpr  10919  enrex  10988  ltrelsr  10989  ltrelre  11055  ltrelxr  11204  rlimpm  15460  dvdszrcl  16224  prdsle  17423  prdsless  17424  sectfval  17716  sectss  17717  ltbval  22026  opsrle  22030  lmfval  23222  isphtpc  24986  bcthlem1  25316  bcthlem5  25320  lgsquadlem1  27368  lgsquadlem2  27369  lgsquadlem3  27370  ishlg  28695  perpln1  28803  perpln2  28804  isperp  28805  iscgra  28902  isinag  28931  isleag  28940  inftmrel  33268  isinftm  33269  fldextfld1  33838  fldextfld2  33839  metidval  34081  metidss  34082  faeval  34437  filnetlem2  36614  numiunnum  36705  areacirc  38087  lcvfbr  39519  cmtfvalN  39709  cvrfval  39767  dicssdvh  41685  aks6d1c1p1rcl  42600  pellexlem3  43283  pellexlem4  43284  pellexlem5  43285  pellex  43287  rfovcnvf1od  44455  fsovrfovd  44460  sectfn  49526