Theorem opabssxp 5758

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

This proof depends on syntax axioms:   ∧ wa 401   ∈ wcel 2146   ⊆ wss 3908  {copab 5178   × cxp 5664

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 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-ss 3925  df-opab 5179  df-xp 5672

This theorem is used by:  brab2a  5759  dmoprabss  7527  ecopovsym  8826  ecopovtrn  8827  ecopover  8828  enqex  10925  lterpq  10973  ltrelpr  11001  enrex  11070  ltrelsr  11071  ltrelre  11137  ltrelxr  11288  rlimpm  15577  dvdszrcl  16340  prdsle  17540  prdsless  17541  sectfval  17833  sectss  17834  ltbval  22231  opsrle  22235  lmfval  23426  isphtpc  25190  bcthlem1  25520  bcthlem5  25524  lgsquadlem1  27581  lgsquadlem2  27582  lgsquadlem3  27583  ishlg2  28908  ishlg  28911  perpln1  29027  perpln2  29028  isperp  29029  iscgra  29157  isinag  29192  isleag  29201  inftmrel  33531  isinftm  33532  fldextfld1  34068  fldextfld2  34069  metidval  34311  metidss  34312  faeval  34668  filnetlem2  36931  numiunnum  37022  areacirc  38405  lcvfbr  39835  cmtfvalN  40025  cvrfval  40083  dicssdvh  42001  aks6d1c1p1rcl  42916  pellexlem3  43599  pellexlem4  43600  pellexlem5  43601  pellex  43603  rfovcnvf1od  44771  fsovrfovd  44776  sectfn  49848