Theorem opabssxp 5792

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

Syntax hints:   ∧ wa 395   ∈ wcel 2108   ⊆ wss 3976  {copab 5228   × cxp 5698

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-ss 3993  df-opab 5229  df-xp 5706

This theorem is referenced by:  brab2a  5793  dmoprabss  7553  ecopovsym  8877  ecopovtrn  8878  ecopover  8879  enqex  10991  lterpq  11039  ltrelpr  11067  enrex  11136  ltrelsr  11137  ltrelre  11203  ltrelxr  11351  rlimpm  15546  dvdszrcl  16307  prdsle  17522  prdsless  17523  sectfval  17812  sectss  17813  ltbval  22084  opsrle  22088  lmfval  23261  isphtpc  25045  bcthlem1  25377  bcthlem5  25381  lgsquadlem1  27442  lgsquadlem2  27443  lgsquadlem3  27444  ishlg  28628  perpln1  28736  perpln2  28737  isperp  28738  iscgra  28835  isinag  28864  isleag  28873  inftmrel  33160  isinftm  33161  fldextfld1  33662  fldextfld2  33663  metidval  33836  metidss  33837  faeval  34210  filnetlem2  36345  numiunnum  36436  areacirc  37673  lcvfbr  38976  cmtfvalN  39166  cvrfval  39224  dicssdvh  41143  aks6d1c1p1rcl  42065  pellexlem3  42787  pellexlem4  42788  pellexlem5  42789  pellex  42791  rfovcnvf1od  43966  fsovrfovd  43971