Theorem opabssxp 5734

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

Syntax hints:   ∧ wa 395   ∈ wcel 2109   ⊆ wss 3917  {copab 5172   × cxp 5639

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-ss 3934  df-opab 5173  df-xp 5647

This theorem is referenced by:  brab2a  5735  dmoprabss  7496  ecopovsym  8795  ecopovtrn  8796  ecopover  8797  enqex  10882  lterpq  10930  ltrelpr  10958  enrex  11027  ltrelsr  11028  ltrelre  11094  ltrelxr  11242  rlimpm  15473  dvdszrcl  16234  prdsle  17432  prdsless  17433  sectfval  17720  sectss  17721  ltbval  21957  opsrle  21961  lmfval  23126  isphtpc  24900  bcthlem1  25231  bcthlem5  25235  lgsquadlem1  27298  lgsquadlem2  27299  lgsquadlem3  27300  ishlg  28536  perpln1  28644  perpln2  28645  isperp  28646  iscgra  28743  isinag  28772  isleag  28781  inftmrel  33141  isinftm  33142  fldextfld1  33650  fldextfld2  33651  metidval  33887  metidss  33888  faeval  34243  filnetlem2  36374  numiunnum  36465  areacirc  37714  lcvfbr  39020  cmtfvalN  39210  cvrfval  39268  dicssdvh  41187  aks6d1c1p1rcl  42103  pellexlem3  42826  pellexlem4  42827  pellexlem5  42828  pellex  42830  rfovcnvf1od  44000  fsovrfovd  44005  sectfn  49022