Theorem opabssxp 5751

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

This proof depends on syntax axioms:   ∧ wa 401   ∈ wcel 2145   ⊆ wss 3902  {copab 5171   × cxp 5657

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 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-ss 3919  df-opab 5172  df-xp 5665

This theorem is used by:  brab2a  5752  dmoprabss  7521  ecopovsym  8823  ecopovtrn  8824  ecopover  8825  enqex  10935  lterpq  10983  ltrelpr  11011  enrex  11080  ltrelsr  11081  ltrelre  11147  ltrelxr  11298  rlimpm  15591  dvdszrcl  16353  prdsle  17553  prdsless  17554  sectfval  17846  sectss  17847  ltbval  22265  opsrle  22269  lmfval  23463  isphtpc  25228  bcthlem1  25558  bcthlem5  25562  lgsquadlem1  27624  lgsquadlem2  27625  lgsquadlem3  27626  ishlg2  28952  ishlg  28955  perpln1  29072  perpln2  29073  isperp  29074  iscgra  29203  isinag  29244  isleag  29253  inftmrel  33628  isinftm  33629  fldextfld1  34165  fldextfld2  34166  metidval  34408  metidss  34409  faeval  34765  filnetlem2  37006  numiunnum  37097  areacirc  38470  lcvfbr  39901  cmtfvalN  40091  cvrfval  40149  dicssdvh  42067  aks6d1c1p1rcl  42982  pellexlem3  43680  pellexlem4  43681  pellexlem5  43682  pellex  43684  rfovcnvf1od  44852  fsovrfovd  44857  sectfn  49963