Theorem opabssxp 5711

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

Syntax hints:   ∧ wa 395   ∈ wcel 2109   ⊆ wss 3903  {copab 5154   × cxp 5617

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 3920  df-opab 5155  df-xp 5625

This theorem is referenced by:  brab2a  5712  dmoprabss  7453  ecopovsym  8746  ecopovtrn  8747  ecopover  8748  enqex  10816  lterpq  10864  ltrelpr  10892  enrex  10961  ltrelsr  10962  ltrelre  11028  ltrelxr  11176  rlimpm  15407  dvdszrcl  16168  prdsle  17366  prdsless  17367  sectfval  17658  sectss  17659  ltbval  21948  opsrle  21952  lmfval  23117  isphtpc  24891  bcthlem1  25222  bcthlem5  25226  lgsquadlem1  27289  lgsquadlem2  27290  lgsquadlem3  27291  ishlg  28551  perpln1  28659  perpln2  28660  isperp  28661  iscgra  28758  isinag  28787  isleag  28796  inftmrel  33131  isinftm  33132  fldextfld1  33630  fldextfld2  33631  metidval  33873  metidss  33874  faeval  34229  filnetlem2  36373  numiunnum  36464  areacirc  37713  lcvfbr  39019  cmtfvalN  39209  cvrfval  39267  dicssdvh  41185  aks6d1c1p1rcl  42101  pellexlem3  42824  pellexlem4  42825  pellexlem5  42826  pellex  42828  rfovcnvf1od  43997  fsovrfovd  44002  sectfn  49034