Theorem opabssxp 5749

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

This proof depends on syntax axioms:   ∧ wa 401   ∈ wcel 2147   ⊆ wss 3900  {copab 5171   × cxp 5654

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-ss 3901  df-opab 5172  df-xp 5662

This theorem is used by:  brab2a  5750  dmoprabss  7550  ecopovsym  8871  ecopovtrn  8872  ecopover  8873  enqex  11037  lterpq  11085  ltrelpr  11113  enrex  11182  ltrelsr  11183  ltrelre  11249  ltrelxr  11400  rlimpm  15699  dvdszrcl  16459  prdsle  17665  prdsless  17666  sectfval  17958  sectss  17959  ltbval  22385  opsrle  22389  lmfval  23583  isphtpc  25348  bcthlem1  25678  bcthlem5  25682  lgsquadlem1  27740  lgsquadlem2  27741  lgsquadlem3  27742  ishlg2  29098  ishlg  29101  perpln1  29218  perpln2  29219  isperp  29220  iscgra  29349  isinag  29390  isleag  29399  inftmrel  33817  isinftm  33818  fldextfld1  34362  fldextfld2  34363  metidval  34605  metidss  34606  faeval  34962  filnetlem2  37358  numiunnum  37449  areacirc  38836  lcvfbr  40280  cmtfvalN  40470  cvrfval  40528  dicssdvh  42446  aks6d1c1p1rcl  43361  pellexlem3  44042  pellexlem4  44043  pellexlem5  44044  pellex  44046  rfovcnvf1od  45207  fsovrfovd  45212  sectfn  50358