Theorem opabssxp 5737

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

Syntax hints:   ∧ wa 399   ∈ wcel 2141   ⊆ wss 3904  {copab 5161   × cxp 5643

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-ss 3921  df-opab 5162  df-xp 5651

This theorem is referenced by:  brab2a  5738  dmoprabss  7496  ecopovsym  8796  ecopovtrn  8797  ecopover  8798  enqex  10877  lterpq  10925  ltrelpr  10953  enrex  11022  ltrelsr  11023  ltrelre  11089  ltrelxr  11240  rlimpm  15510  dvdszrcl  16274  prdsle  17474  prdsless  17475  sectfval  17767  sectss  17768  ltbval  22076  opsrle  22080  lmfval  23272  isphtpc  25036  bcthlem1  25366  bcthlem5  25370  lgsquadlem1  27421  lgsquadlem2  27422  lgsquadlem3  27423  ishlg  28748  perpln1  28856  perpln2  28857  isperp  28858  iscgra  28955  isinag  28984  isleag  28993  inftmrel  33321  isinftm  33322  fldextfld1  33905  fldextfld2  33906  metidval  34148  metidss  34149  faeval  34504  filnetlem2  36703  numiunnum  36794  areacirc  38176  lcvfbr  39608  cmtfvalN  39798  cvrfval  39856  dicssdvh  41774  aks6d1c1p1rcl  42689  pellexlem3  43372  pellexlem4  43373  pellexlem5  43374  pellex  43376  rfovcnvf1od  44544  fsovrfovd  44549  sectfn  49614