Theorem opabssxp 5669

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

Syntax hints:   ∧ wa 395   ∈ wcel 2108   ⊆ wss 3883  {copab 5132   × cxp 5578

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900  df-opab 5133  df-xp 5586

This theorem is referenced by:  brab2a  5670  dmoprabss  7355  ecopovsym  8566  ecopovtrn  8567  ecopover  8568  enqex  10609  lterpq  10657  ltrelpr  10685  enrex  10754  ltrelsr  10755  ltrelre  10821  ltrelxr  10967  rlimpm  15137  dvdszrcl  15896  prdsle  17090  prdsless  17091  sectfval  17380  sectss  17381  ltbval  21154  opsrle  21158  lmfval  22291  isphtpc  24063  bcthlem1  24393  bcthlem5  24397  lgsquadlem1  26433  lgsquadlem2  26434  lgsquadlem3  26435  ishlg  26867  perpln1  26975  perpln2  26976  isperp  26977  iscgra  27074  isinag  27103  isleag  27112  inftmrel  31336  isinftm  31337  fldextfld1  31626  fldextfld2  31627  metidval  31742  metidss  31743  faeval  32114  filnetlem2  34495  areacirc  35797  lcvfbr  36961  cmtfvalN  37151  cvrfval  37209  dicssdvh  39127  pellexlem3  40569  pellexlem4  40570  pellexlem5  40571  pellex  40573  rfovcnvf1od  41501  fsovrfovd  41506