Theorem opabssxp 5643

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

Syntax hints:   ∧ wa 398   ∈ wcel 2114   ⊆ wss 3936  {copab 5128   × cxp 5553

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-in 3943  df-ss 3952  df-opab 5129  df-xp 5561

This theorem is referenced by:  brab2a  5644  dmoprabss  7256  ecopovsym  8399  ecopovtrn  8400  ecopover  8401  enqex  10344  lterpq  10392  ltrelpr  10420  enrex  10489  ltrelsr  10490  ltrelre  10556  ltrelxr  10702  rlimpm  14857  dvdszrcl  15612  prdsle  16735  prdsless  16736  sectfval  17021  sectss  17022  ltbval  20252  opsrle  20256  lmfval  21840  isphtpc  23598  bcthlem1  23927  bcthlem5  23931  lgsquadlem1  25956  lgsquadlem2  25957  lgsquadlem3  25958  ishlg  26388  perpln1  26496  perpln2  26497  isperp  26498  iscgra  26595  isinag  26624  isleag  26633  inftmrel  30809  isinftm  30810  fldextfld1  31039  fldextfld2  31040  metidval  31130  metidss  31131  faeval  31505  filnetlem2  33727  areacirc  35002  lcvfbr  36171  cmtfvalN  36361  cvrfval  36419  dicssdvh  38337  pellexlem3  39477  pellexlem4  39478  pellexlem5  39479  pellex  39481  rfovcnvf1od  40399  fsovrfovd  40404