Theorem opabssxp 5679

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

Syntax hints:   ∧ wa 396   ∈ wcel 2110   ⊆ wss 3892  {copab 5141   × cxp 5588

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1545  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-v 3433  df-in 3899  df-ss 3909  df-opab 5142  df-xp 5596

This theorem is referenced by:  brab2a  5680  dmoprabss  7371  ecopovsym  8591  ecopovtrn  8592  ecopover  8593  enqex  10679  lterpq  10727  ltrelpr  10755  enrex  10824  ltrelsr  10825  ltrelre  10891  ltrelxr  11037  rlimpm  15207  dvdszrcl  15966  prdsle  17171  prdsless  17172  sectfval  17461  sectss  17462  ltbval  21242  opsrle  21246  lmfval  22381  isphtpc  24155  bcthlem1  24486  bcthlem5  24490  lgsquadlem1  26526  lgsquadlem2  26527  lgsquadlem3  26528  ishlg  26961  perpln1  27069  perpln2  27070  isperp  27071  iscgra  27168  isinag  27197  isleag  27206  inftmrel  31430  isinftm  31431  fldextfld1  31720  fldextfld2  31721  metidval  31836  metidss  31837  faeval  32210  filnetlem2  34564  areacirc  35866  lcvfbr  37030  cmtfvalN  37220  cvrfval  37278  dicssdvh  39196  pellexlem3  40650  pellexlem4  40651  pellexlem5  40652  pellex  40654  rfovcnvf1od  41582  fsovrfovd  41587