Theorem opabssxp 5227

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 472	. . 3 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
2	1	ssopab2i 5032	. 2 ⊢ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)} ⊆ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}
3		df-xp 5149	. 2 ⊢ (𝐴 × 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}
4	2, 3	sseqtr4i 3671	1 ⊢ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)} ⊆ (𝐴 × 𝐵)

Syntax hints:   ∧ wa 383   ∈ wcel 2030   ⊆ wss 3607  {copab 4745   × cxp 5141

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-in 3614  df-ss 3621  df-opab 4746  df-xp 5149

This theorem is referenced by:  brab2a  5228  dmoprabss  6784  ecopovsym  7892  ecopovtrn  7893  ecopover  7894  enqex  9782  lterpq  9830  ltrelpr  9858  enrex  9926  ltrelsr  9927  ltrelre  9993  ltrelxr  10137  rlimpm  14275  dvdszrcl  15032  prdsle  16169  prdsless  16170  sectfval  16458  sectss  16459  ltbval  19519  opsrle  19523  lmfval  21084  isphtpc  22840  bcthlem1  23167  bcthlem5  23171  lgsquadlem1  25150  lgsquadlem2  25151  lgsquadlem3  25152  ishlg  25542  perpln1  25650  perpln2  25651  isperp  25652  iscgra  25746  isinag  25774  isleag  25778  inftmrel  29862  isinftm  29863  metidval  30061  metidss  30062  faeval  30437  filnetlem2  32499  areacirc  33635  lcvfbr  34625  cmtfvalN  34815  cvrfval  34873  dicssdvh  36792  pellexlem3  37712  pellexlem4  37713  pellexlem5  37714  pellex  37716  rfovcnvf1od  38615  fsovrfovd  38620