Theorem opabssxp 5742

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

This proof depends on syntax axioms:   ∧ wa 401   ∈ wcel 2144   ⊆ wss 3895  {copab 5166   × cxp 5648

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-ss 3896  df-opab 5167  df-xp 5656

This theorem is used by:  brab2a  5743  dmoprabss  7525  ecopovsym  8844  ecopovtrn  8845  ecopover  8846  enqex  11011  lterpq  11059  ltrelpr  11087  enrex  11156  ltrelsr  11157  ltrelre  11223  ltrelxr  11374  rlimpm  15673  dvdszrcl  16433  prdsle  17639  prdsless  17640  sectfval  17932  sectss  17933  ltbval  22358  opsrle  22362  lmfval  23556  isphtpc  25321  bcthlem1  25651  bcthlem5  25655  lgsquadlem1  27713  lgsquadlem2  27714  lgsquadlem3  27715  ishlg2  29071  ishlg  29074  perpln1  29191  perpln2  29192  isperp  29193  iscgra  29322  isinag  29363  isleag  29372  inftmrel  33788  isinftm  33789  fldextfld1  34326  fldextfld2  34327  metidval  34569  metidss  34570  faeval  34926  filnetlem2  37260  numiunnum  37351  areacirc  38725  lcvfbr  40171  cmtfvalN  40361  cvrfval  40419  dicssdvh  42337  aks6d1c1p1rcl  43252  pellexlem3  43932  pellexlem4  43933  pellexlem5  43934  pellex  43936  rfovcnvf1od  45098  fsovrfovd  45103  sectfn  50237