Theorem opabssxp 5743

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

This proof depends on syntax axioms:   ∧ wa 401   ∈ wcel 2145   ⊆ wss 3899  {copab 5167   × cxp 5649

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-ss 3916  df-opab 5168  df-xp 5657

This theorem is used by:  brab2a  5744  dmoprabss  7516  ecopovsym  8824  ecopovtrn  8825  ecopover  8826  enqex  10988  lterpq  11036  ltrelpr  11064  enrex  11133  ltrelsr  11134  ltrelre  11200  ltrelxr  11351  rlimpm  15647  dvdszrcl  16407  prdsle  17613  prdsless  17614  sectfval  17906  sectss  17907  ltbval  22332  opsrle  22336  lmfval  23530  isphtpc  25295  bcthlem1  25625  bcthlem5  25629  lgsquadlem1  27689  lgsquadlem2  27690  lgsquadlem3  27691  ishlg2  29047  ishlg  29050  perpln1  29167  perpln2  29168  isperp  29169  iscgra  29298  isinag  29339  isleag  29348  inftmrel  33723  isinftm  33724  fldextfld1  34261  fldextfld2  34262  metidval  34504  metidss  34505  faeval  34861  filnetlem2  37137  numiunnum  37228  areacirc  38599  lcvfbr  40045  cmtfvalN  40235  cvrfval  40293  dicssdvh  42211  aks6d1c1p1rcl  43126  pellexlem3  43791  pellexlem4  43792  pellexlem5  43793  pellex  43795  rfovcnvf1od  44963  fsovrfovd  44968  sectfn  50081