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 3972	1 ⊢ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)} ⊆ (𝐴 × 𝐵)

Syntax hints:   ∧ wa 395   ∈ wcel 2114   ⊆ wss 3890  {copab 5148   × cxp 5622

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-ss 3907  df-opab 5149  df-xp 5630

This theorem is referenced by:  brab2a  5717  dmoprabss  7464  ecopovsym  8759  ecopovtrn  8760  ecopover  8761  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  22031  opsrle  22035  lmfval  23207  isphtpc  24971  bcthlem1  25301  bcthlem5  25305  lgsquadlem1  27357  lgsquadlem2  27358  lgsquadlem3  27359  ishlg  28684  perpln1  28792  perpln2  28793  isperp  28794  iscgra  28891  isinag  28920  isleag  28929  inftmrel  33256  isinftm  33257  fldextfld1  33807  fldextfld2  33808  metidval  34050  metidss  34051  faeval  34406  filnetlem2  36577  numiunnum  36668  areacirc  38048  lcvfbr  39480  cmtfvalN  39670  cvrfval  39728  dicssdvh  41646  aks6d1c1p1rcl  42561  pellexlem3  43277  pellexlem4  43278  pellexlem5  43279  pellex  43281  rfovcnvf1od  44449  fsovrfovd  44454  sectfn  49516