Theorem opabssxp 5766

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

Syntax hints:   ∧ wa 396   ∈ wcel 2106   ⊆ wss 3947  {copab 5209   × cxp 5673

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3954  df-ss 3964  df-opab 5210  df-xp 5681

This theorem is referenced by:  brab2a  5767  dmoprabss  7507  ecopovsym  8809  ecopovtrn  8810  ecopover  8811  enqex  10913  lterpq  10961  ltrelpr  10989  enrex  11058  ltrelsr  11059  ltrelre  11125  ltrelxr  11271  rlimpm  15440  dvdszrcl  16198  prdsle  17404  prdsless  17405  sectfval  17694  sectss  17695  ltbval  21589  opsrle  21593  lmfval  22727  isphtpc  24501  bcthlem1  24832  bcthlem5  24836  lgsquadlem1  26872  lgsquadlem2  26873  lgsquadlem3  26874  ishlg  27842  perpln1  27950  perpln2  27951  isperp  27952  iscgra  28049  isinag  28078  isleag  28087  inftmrel  32313  isinftm  32314  fldextfld1  32716  fldextfld2  32717  metidval  32858  metidss  32859  faeval  33232  filnetlem2  35252  areacirc  36569  lcvfbr  37878  cmtfvalN  38068  cvrfval  38126  dicssdvh  40045  pellexlem3  41554  pellexlem4  41555  pellexlem5  41556  pellex  41558  rfovcnvf1od  42740  fsovrfovd  42745