Theorem opabssxp 5767

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

Syntax hints:   ∧ wa 394   ∈ wcel 2104   ⊆ wss 3947  {copab 5209   × cxp 5673

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-v 3474  df-in 3954  df-ss 3964  df-opab 5210  df-xp 5681

This theorem is referenced by:  brab2a  5768  dmoprabss  7513  ecopovsym  8815  ecopovtrn  8816  ecopover  8817  enqex  10919  lterpq  10967  ltrelpr  10995  enrex  11064  ltrelsr  11065  ltrelre  11131  ltrelxr  11279  rlimpm  15448  dvdszrcl  16206  prdsle  17412  prdsless  17413  sectfval  17702  sectss  17703  ltbval  21817  opsrle  21821  lmfval  22956  isphtpc  24740  bcthlem1  25072  bcthlem5  25076  lgsquadlem1  27119  lgsquadlem2  27120  lgsquadlem3  27121  ishlg  28120  perpln1  28228  perpln2  28229  isperp  28230  iscgra  28327  isinag  28356  isleag  28365  inftmrel  32596  isinftm  32597  fldextfld1  33016  fldextfld2  33017  metidval  33168  metidss  33169  faeval  33542  filnetlem2  35567  areacirc  36884  lcvfbr  38193  cmtfvalN  38383  cvrfval  38441  dicssdvh  40360  pellexlem3  41871  pellexlem4  41872  pellexlem5  41873  pellex  41875  rfovcnvf1od  43057  fsovrfovd  43062