Theorem opabssxp 5731

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

Syntax hints:   ∧ wa 395   ∈ wcel 2109   ⊆ wss 3914  {copab 5169   × cxp 5636

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-ss 3931  df-opab 5170  df-xp 5644

This theorem is referenced by:  brab2a  5732  dmoprabss  7493  ecopovsym  8792  ecopovtrn  8793  ecopover  8794  enqex  10875  lterpq  10923  ltrelpr  10951  enrex  11020  ltrelsr  11021  ltrelre  11087  ltrelxr  11235  rlimpm  15466  dvdszrcl  16227  prdsle  17425  prdsless  17426  sectfval  17713  sectss  17714  ltbval  21950  opsrle  21954  lmfval  23119  isphtpc  24893  bcthlem1  25224  bcthlem5  25228  lgsquadlem1  27291  lgsquadlem2  27292  lgsquadlem3  27293  ishlg  28529  perpln1  28637  perpln2  28638  isperp  28639  iscgra  28736  isinag  28765  isleag  28774  inftmrel  33134  isinftm  33135  fldextfld1  33643  fldextfld2  33644  metidval  33880  metidss  33881  faeval  34236  filnetlem2  36367  numiunnum  36458  areacirc  37707  lcvfbr  39013  cmtfvalN  39203  cvrfval  39261  dicssdvh  41180  aks6d1c1p1rcl  42096  pellexlem3  42819  pellexlem4  42820  pellexlem5  42821  pellex  42823  rfovcnvf1od  43993  fsovrfovd  43998  sectfn  49018