Theorem opabssxp 5607

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 486	. . 3 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
2	1	ssopab2i 5402	. 2 ⊢ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)} ⊆ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}
3		df-xp 5525	. 2 ⊢ (𝐴 × 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}
4	2, 3	sseqtrri 3952	1 ⊢ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)} ⊆ (𝐴 × 𝐵)

Syntax hints:   ∧ wa 399   ∈ wcel 2111   ⊆ wss 3881  {copab 5092   × cxp 5517

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898  df-opab 5093  df-xp 5525

This theorem is referenced by:  brab2a  5608  dmoprabss  7235  ecopovsym  8382  ecopovtrn  8383  ecopover  8384  enqex  10333  lterpq  10381  ltrelpr  10409  enrex  10478  ltrelsr  10479  ltrelre  10545  ltrelxr  10691  rlimpm  14849  dvdszrcl  15604  prdsle  16727  prdsless  16728  sectfval  17013  sectss  17014  ltbval  20711  opsrle  20715  lmfval  21837  isphtpc  23599  bcthlem1  23928  bcthlem5  23932  lgsquadlem1  25964  lgsquadlem2  25965  lgsquadlem3  25966  ishlg  26396  perpln1  26504  perpln2  26505  isperp  26506  iscgra  26603  isinag  26632  isleag  26641  inftmrel  30859  isinftm  30860  fldextfld1  31127  fldextfld2  31128  metidval  31243  metidss  31244  faeval  31615  filnetlem2  33840  areacirc  35150  lcvfbr  36316  cmtfvalN  36506  cvrfval  36564  dicssdvh  38482  pellexlem3  39772  pellexlem4  39773  pellexlem5  39774  pellex  39776  rfovcnvf1od  40705  fsovrfovd  40710