Theorem opabssxp 5715

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

Syntax hints:   ∧ wa 395   ∈ wcel 2109   ⊆ wss 3905  {copab 5157   × cxp 5621

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-ss 3922  df-opab 5158  df-xp 5629

This theorem is referenced by:  brab2a  5716  dmoprabss  7457  ecopovsym  8753  ecopovtrn  8754  ecopover  8755  enqex  10835  lterpq  10883  ltrelpr  10911  enrex  10980  ltrelsr  10981  ltrelre  11047  ltrelxr  11195  rlimpm  15425  dvdszrcl  16186  prdsle  17384  prdsless  17385  sectfval  17676  sectss  17677  ltbval  21966  opsrle  21970  lmfval  23135  isphtpc  24909  bcthlem1  25240  bcthlem5  25244  lgsquadlem1  27307  lgsquadlem2  27308  lgsquadlem3  27309  ishlg  28565  perpln1  28673  perpln2  28674  isperp  28675  iscgra  28772  isinag  28801  isleag  28810  inftmrel  33132  isinftm  33133  fldextfld1  33619  fldextfld2  33620  metidval  33856  metidss  33857  faeval  34212  filnetlem2  36352  numiunnum  36443  areacirc  37692  lcvfbr  38998  cmtfvalN  39188  cvrfval  39246  dicssdvh  41165  aks6d1c1p1rcl  42081  pellexlem3  42804  pellexlem4  42805  pellexlem5  42806  pellex  42808  rfovcnvf1od  43977  fsovrfovd  43982  sectfn  49015