Theorem opabssxp 5716

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

Syntax hints:   ∧ wa 395   ∈ wcel 2113   ⊆ wss 3901  {copab 5160   × cxp 5622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-ss 3918  df-opab 5161  df-xp 5630

This theorem is referenced by:  brab2a  5717  dmoprabss  7462  ecopovsym  8756  ecopovtrn  8757  ecopover  8758  enqex  10833  lterpq  10881  ltrelpr  10909  enrex  10978  ltrelsr  10979  ltrelre  11045  ltrelxr  11193  rlimpm  15423  dvdszrcl  16184  prdsle  17382  prdsless  17383  sectfval  17675  sectss  17676  ltbval  21998  opsrle  22002  lmfval  23176  isphtpc  24949  bcthlem1  25280  bcthlem5  25284  lgsquadlem1  27347  lgsquadlem2  27348  lgsquadlem3  27349  ishlg  28674  perpln1  28782  perpln2  28783  isperp  28784  iscgra  28881  isinag  28910  isleag  28919  inftmrel  33262  isinftm  33263  fldextfld1  33804  fldextfld2  33805  metidval  34047  metidss  34048  faeval  34403  filnetlem2  36573  numiunnum  36664  areacirc  37910  lcvfbr  39276  cmtfvalN  39466  cvrfval  39524  dicssdvh  41442  aks6d1c1p1rcl  42358  pellexlem3  43069  pellexlem4  43070  pellexlem5  43071  pellex  43073  rfovcnvf1od  44241  fsovrfovd  44246  sectfn  49270