Home Intuitionistic Logic ExplorerTheorem List (p. 45 of 114) < Previous  Next > Bad symbols? Try the GIF version. Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Intuitionistic Logic Explorer - 4401-4500   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremnnsuc 4401* A nonzero natural number is a successor. (Contributed by NM, 18-Feb-2004.)
((𝐴 ∈ ω ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ ω 𝐴 = suc 𝑥)

Theoremnndceq0 4402 A natural number is either zero or nonzero. Decidable equality for natural numbers is a special case of the law of the excluded middle which holds in most constructive set theories including ours. (Contributed by Jim Kingdon, 5-Jan-2019.)
(𝐴 ∈ ω → DECID 𝐴 = ∅)

Theorem0elnn 4403 A natural number is either the empty set or has the empty set as an element. (Contributed by Jim Kingdon, 23-Aug-2019.)
(𝐴 ∈ ω → (𝐴 = ∅ ∨ ∅ ∈ 𝐴))

Theoremnn0eln0 4404 A natural number is nonempty iff it contains the empty set. Although in constructive mathematics it is generally more natural to work with inhabited sets and ignore the whole concept of nonempty sets, in the specific case of natural numbers this theorem may be helpful in converting proofs which were written assuming excluded middle. (Contributed by Jim Kingdon, 28-Aug-2019.)
(𝐴 ∈ ω → (∅ ∈ 𝐴𝐴 ≠ ∅))

Theoremnnregexmid 4405* If inhabited sets of natural numbers always have minimal elements, excluded middle follows. The argument is essentially the same as regexmid 4322 and the larger lesson is that although natural numbers may behave "non-constructively" even in a constructive set theory (for example see nndceq 6207 or nntri3or 6201), sets of natural numbers are a different animal. (Contributed by Jim Kingdon, 6-Sep-2019.)
((𝑥 ⊆ ω ∧ ∃𝑦 𝑦𝑥) → ∃𝑦(𝑦𝑥 ∧ ∀𝑧(𝑧𝑦 → ¬ 𝑧𝑥)))       (𝜑 ∨ ¬ 𝜑)

Theoremomsinds 4406* Strong (or "total") induction principle over ω. (Contributed by Scott Fenton, 17-Jul-2015.)
(𝑥 = 𝑦 → (𝜑𝜓))    &   (𝑥 = 𝐴 → (𝜑𝜒))    &   (𝑥 ∈ ω → (∀𝑦𝑥 𝜓𝜑))       (𝐴 ∈ ω → 𝜒)

2.6.6  Relations

Syntaxcxp 4407 Extend the definition of a class to include the cross product.
class (𝐴 × 𝐵)

Syntaxccnv 4408 Extend the definition of a class to include the converse of a class.
class 𝐴

Syntaxcdm 4409 Extend the definition of a class to include the domain of a class.
class dom 𝐴

Syntaxcrn 4410 Extend the definition of a class to include the range of a class.
class ran 𝐴

Syntaxcres 4411 Extend the definition of a class to include the restriction of a class. (Read: The restriction of 𝐴 to 𝐵.)
class (𝐴𝐵)

Syntaxcima 4412 Extend the definition of a class to include the image of a class. (Read: The image of 𝐵 under 𝐴.)
class (𝐴𝐵)

Syntaxccom 4413 Extend the definition of a class to include the composition of two classes. (Read: The composition of 𝐴 and 𝐵.)
class (𝐴𝐵)

Syntaxwrel 4414 Extend the definition of a wff to include the relation predicate. (Read: 𝐴 is a relation.)
wff Rel 𝐴

Definitiondf-xp 4415* Define the cross product of two classes. Definition 9.11 of [Quine] p. 64. For example, ( { 1 , 5 } × { 2 , 7 } ) = ( { 1 , 2 , 1 , 7 } { 5 , 2 , 5 , 7 } ) . Another example is that the set of rational numbers are defined in using the cross-product ( Z × N ) ; the left- and right-hand sides of the cross-product represent the top (integer) and bottom (natural) numbers of a fraction. (Contributed by NM, 4-Jul-1994.)
(𝐴 × 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐵)}

Definitiondf-rel 4416 Define the relation predicate. Definition 6.4(1) of [TakeutiZaring] p. 23. For alternate definitions, see dfrel2 4843 and dfrel3 4850. (Contributed by NM, 1-Aug-1994.)
(Rel 𝐴𝐴 ⊆ (V × V))

Definitiondf-cnv 4417* Define the converse of a class. Definition 9.12 of [Quine] p. 64. The converse of a binary relation swaps its arguments, i.e., if 𝐴 ∈ V and 𝐵 ∈ V then (𝐴𝑅𝐵𝐵𝑅𝐴), as proven in brcnv 4585 (see df-br 3820 and df-rel 4416 for more on relations). For example, { 2 , 6 , 3 , 9 } = { 6 , 2 , 9 , 3 } . We use Quine's breve accent (smile) notation. Like Quine, we use it as a prefix, which eliminates the need for parentheses. Many authors use the postfix superscript "to the minus one." "Converse" is Quine's terminology; some authors call it "inverse," especially when the argument is a function. (Contributed by NM, 4-Jul-1994.)
𝐴 = {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐴𝑥}

Definitiondf-co 4418* Define the composition of two classes. Definition 6.6(3) of [TakeutiZaring] p. 24. Note that Definition 7 of [Suppes] p. 63 reverses 𝐴 and 𝐵, uses a slash instead of , and calls the operation "relative product." (Contributed by NM, 4-Jul-1994.)
(𝐴𝐵) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐵𝑧𝑧𝐴𝑦)}

Definitiondf-dm 4419* Define the domain of a class. Definition 3 of [Suppes] p. 59. For example, F = { 2 , 6 , 3 , 9 } dom F = { 2 , 3 } . Contrast with range (defined in df-rn 4420). For alternate definitions see dfdm2 4927, dfdm3 4589, and dfdm4 4594. The notation "dom " is used by Enderton; other authors sometimes use script D. (Contributed by NM, 1-Aug-1994.)
dom 𝐴 = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦}

Definitiondf-rn 4420 Define the range of a class. For example, F = { 2 , 6 , 3 , 9 } -> ran F = { 6 , 9 } . Contrast with domain (defined in df-dm 4419). For alternate definitions, see dfrn2 4590, dfrn3 4591, and dfrn4 4853. The notation "ran " is used by Enderton; other authors sometimes use script R or script W. (Contributed by NM, 1-Aug-1994.)
ran 𝐴 = dom 𝐴

Definitiondf-res 4421 Define the restriction of a class. Definition 6.6(1) of [TakeutiZaring] p. 24. For example ( F = { 2 , 6 , 3 , 9 } B = { 1 , 2 } ) -> ( F B ) = { 2 , 6 } . (Contributed by NM, 2-Aug-1994.)
(𝐴𝐵) = (𝐴 ∩ (𝐵 × V))

Definitiondf-ima 4422 Define the image of a class (as restricted by another class). Definition 6.6(2) of [TakeutiZaring] p. 24. For example, ( F = { 2 , 6 , 3 , 9 } /\ B = { 1 , 2 } ) -> ( F B ) = { 6 } . Contrast with restriction (df-res 4421) and range (df-rn 4420). For an alternate definition, see dfima2 4739. (Contributed by NM, 2-Aug-1994.)
(𝐴𝐵) = ran (𝐴𝐵)

Theoremxpeq1 4423 Equality theorem for cross product. (Contributed by NM, 4-Jul-1994.)
(𝐴 = 𝐵 → (𝐴 × 𝐶) = (𝐵 × 𝐶))

Theoremxpeq2 4424 Equality theorem for cross product. (Contributed by NM, 5-Jul-1994.)
(𝐴 = 𝐵 → (𝐶 × 𝐴) = (𝐶 × 𝐵))

Theoremelxpi 4425* Membership in a cross product. Uses fewer axioms than elxp 4426. (Contributed by NM, 4-Jul-1994.)
(𝐴 ∈ (𝐵 × 𝐶) → ∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥𝐵𝑦𝐶)))

Theoremelxp 4426* Membership in a cross product. (Contributed by NM, 4-Jul-1994.)
(𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥𝐵𝑦𝐶)))

Theoremelxp2 4427* Membership in a cross product. (Contributed by NM, 23-Feb-2004.)
(𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑥𝐵𝑦𝐶 𝐴 = ⟨𝑥, 𝑦⟩)

Theoremxpeq12 4428 Equality theorem for cross product. (Contributed by FL, 31-Aug-2009.)
((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴 × 𝐶) = (𝐵 × 𝐷))

Theoremxpeq1i 4429 Equality inference for cross product. (Contributed by NM, 21-Dec-2008.)
𝐴 = 𝐵       (𝐴 × 𝐶) = (𝐵 × 𝐶)

Theoremxpeq2i 4430 Equality inference for cross product. (Contributed by NM, 21-Dec-2008.)
𝐴 = 𝐵       (𝐶 × 𝐴) = (𝐶 × 𝐵)

Theoremxpeq12i 4431 Equality inference for cross product. (Contributed by FL, 31-Aug-2009.)
𝐴 = 𝐵    &   𝐶 = 𝐷       (𝐴 × 𝐶) = (𝐵 × 𝐷)

Theoremxpeq1d 4432 Equality deduction for cross product. (Contributed by Jeff Madsen, 17-Jun-2010.)
(𝜑𝐴 = 𝐵)       (𝜑 → (𝐴 × 𝐶) = (𝐵 × 𝐶))

Theoremxpeq2d 4433 Equality deduction for cross product. (Contributed by Jeff Madsen, 17-Jun-2010.)
(𝜑𝐴 = 𝐵)       (𝜑 → (𝐶 × 𝐴) = (𝐶 × 𝐵))

Theoremxpeq12d 4434 Equality deduction for cross product. (Contributed by NM, 8-Dec-2013.)
(𝜑𝐴 = 𝐵)    &   (𝜑𝐶 = 𝐷)       (𝜑 → (𝐴 × 𝐶) = (𝐵 × 𝐷))

Theoremnfxp 4435 Bound-variable hypothesis builder for cross product. (Contributed by NM, 15-Sep-2003.) (Revised by Mario Carneiro, 15-Oct-2016.)
𝑥𝐴    &   𝑥𝐵       𝑥(𝐴 × 𝐵)

Theorem0nelxp 4436 The empty set is not a member of a cross product. (Contributed by NM, 2-May-1996.) (Revised by Mario Carneiro, 26-Apr-2015.)
¬ ∅ ∈ (𝐴 × 𝐵)

Theorem0nelelxp 4437 A member of a cross product (ordered pair) doesn't contain the empty set. (Contributed by NM, 15-Dec-2008.)
(𝐶 ∈ (𝐴 × 𝐵) → ¬ ∅ ∈ 𝐶)

Theoremopelxp 4438 Ordered pair membership in a cross product. (Contributed by NM, 15-Nov-1994.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) (Revised by Mario Carneiro, 26-Apr-2015.)
(⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ (𝐴𝐶𝐵𝐷))

Theorembrxp 4439 Binary relation on a cross product. (Contributed by NM, 22-Apr-2004.)
(𝐴(𝐶 × 𝐷)𝐵 ↔ (𝐴𝐶𝐵𝐷))

Theoremopelxpi 4440 Ordered pair membership in a cross product (implication). (Contributed by NM, 28-May-1995.)
((𝐴𝐶𝐵𝐷) → ⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷))

Theoremopelxp1 4441 The first member of an ordered pair of classes in a cross product belongs to first cross product argument. (Contributed by NM, 28-May-2008.) (Revised by Mario Carneiro, 26-Apr-2015.)
(⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) → 𝐴𝐶)

Theoremopelxp2 4442 The second member of an ordered pair of classes in a cross product belongs to second cross product argument. (Contributed by Mario Carneiro, 26-Apr-2015.)
(⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) → 𝐵𝐷)

Theoremotelxp1 4443 The first member of an ordered triple of classes in a cross product belongs to first cross product argument. (Contributed by NM, 28-May-2008.)
(⟨⟨𝐴, 𝐵⟩, 𝐶⟩ ∈ ((𝑅 × 𝑆) × 𝑇) → 𝐴𝑅)

Theoremrabxp 4444* Membership in a class builder restricted to a cross product. (Contributed by NM, 20-Feb-2014.)
(𝑥 = ⟨𝑦, 𝑧⟩ → (𝜑𝜓))       {𝑥 ∈ (𝐴 × 𝐵) ∣ 𝜑} = {⟨𝑦, 𝑧⟩ ∣ (𝑦𝐴𝑧𝐵𝜓)}

Theorembrrelex12 4445 A true binary relation on a relation implies the arguments are sets. (This is a property of our ordered pair definition.) (Contributed by Mario Carneiro, 26-Apr-2015.)
((Rel 𝑅𝐴𝑅𝐵) → (𝐴 ∈ V ∧ 𝐵 ∈ V))

Theorembrrelex 4446 A true binary relation on a relation implies the first argument is a set. (This is a property of our ordered pair definition.) (Contributed by NM, 18-May-2004.) (Revised by Mario Carneiro, 26-Apr-2015.)
((Rel 𝑅𝐴𝑅𝐵) → 𝐴 ∈ V)

Theorembrrelex2 4447 A true binary relation on a relation implies the second argument is a set. (This is a property of our ordered pair definition.) (Contributed by Mario Carneiro, 26-Apr-2015.)
((Rel 𝑅𝐴𝑅𝐵) → 𝐵 ∈ V)

Theorembrrelexi 4448 The first argument of a binary relation exists. (An artifact of our ordered pair definition.) (Contributed by NM, 4-Jun-1998.)
Rel 𝑅       (𝐴𝑅𝐵𝐴 ∈ V)

Theorembrrelex2i 4449 The second argument of a binary relation exists. (An artifact of our ordered pair definition.) (Contributed by Mario Carneiro, 26-Apr-2015.)
Rel 𝑅       (𝐴𝑅𝐵𝐵 ∈ V)

Theoremnprrel 4450 No proper class is related to anything via any relation. (Contributed by Roy F. Longton, 30-Jul-2005.)
Rel 𝑅    &    ¬ 𝐴 ∈ V        ¬ 𝐴𝑅𝐵

Theoremfconstmpt 4451* Representation of a constant function using the mapping operation. (Note that 𝑥 cannot appear free in 𝐵.) (Contributed by NM, 12-Oct-1999.) (Revised by Mario Carneiro, 16-Nov-2013.)
(𝐴 × {𝐵}) = (𝑥𝐴𝐵)

Theoremvtoclr 4452* Variable to class conversion of transitive relation. (Contributed by NM, 9-Jun-1998.) (Revised by Mario Carneiro, 26-Apr-2015.)
Rel 𝑅    &   ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)       ((𝐴𝑅𝐵𝐵𝑅𝐶) → 𝐴𝑅𝐶)

Theoremopelvvg 4453 Ordered pair membership in the universal class of ordered pairs. (Contributed by Mario Carneiro, 3-May-2015.)
((𝐴𝑉𝐵𝑊) → ⟨𝐴, 𝐵⟩ ∈ (V × V))

Theoremopelvv 4454 Ordered pair membership in the universal class of ordered pairs. (Contributed by NM, 22-Aug-2013.) (Revised by Mario Carneiro, 26-Apr-2015.)
𝐴 ∈ V    &   𝐵 ∈ V       𝐴, 𝐵⟩ ∈ (V × V)

Theoremopthprc 4455 Justification theorem for an ordered pair definition that works for any classes, including proper classes. This is a possible definition implied by the footnote in [Jech] p. 78, which says, "The sophisticated reader will not object to our use of a pair of classes." (Contributed by NM, 28-Sep-2003.)
(((𝐴 × {∅}) ∪ (𝐵 × {{∅}})) = ((𝐶 × {∅}) ∪ (𝐷 × {{∅}})) ↔ (𝐴 = 𝐶𝐵 = 𝐷))

Theorembrel 4456 Two things in a binary relation belong to the relation's domain. (Contributed by NM, 17-May-1996.) (Revised by Mario Carneiro, 26-Apr-2015.)
𝑅 ⊆ (𝐶 × 𝐷)       (𝐴𝑅𝐵 → (𝐴𝐶𝐵𝐷))

Theorembrab2a 4457* Ordered pair membership in an ordered pair class abstraction. (Contributed by Mario Carneiro, 9-Nov-2015.)
((𝑥 = 𝐴𝑦 = 𝐵) → (𝜑𝜓))    &   𝑅 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐶𝑦𝐷) ∧ 𝜑)}       (𝐴𝑅𝐵 ↔ ((𝐴𝐶𝐵𝐷) ∧ 𝜓))

Theoremelxp3 4458* Membership in a cross product. (Contributed by NM, 5-Mar-1995.)
(𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑥𝑦(⟨𝑥, 𝑦⟩ = 𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ (𝐵 × 𝐶)))

Theoremopeliunxp 4459 Membership in a union of cross products. (Contributed by Mario Carneiro, 29-Dec-2014.) (Revised by Mario Carneiro, 1-Jan-2017.)
(⟨𝑥, 𝐶⟩ ∈ 𝑥𝐴 ({𝑥} × 𝐵) ↔ (𝑥𝐴𝐶𝐵))

Theoremxpundi 4460 Distributive law for cross product over union. Theorem 103 of [Suppes] p. 52. (Contributed by NM, 12-Aug-2004.)
(𝐴 × (𝐵𝐶)) = ((𝐴 × 𝐵) ∪ (𝐴 × 𝐶))

Theoremxpundir 4461 Distributive law for cross product over union. Similar to Theorem 103 of [Suppes] p. 52. (Contributed by NM, 30-Sep-2002.)
((𝐴𝐵) × 𝐶) = ((𝐴 × 𝐶) ∪ (𝐵 × 𝐶))

Theoremxpiundi 4462* Distributive law for cross product over indexed union. (Contributed by Mario Carneiro, 27-Apr-2014.)
(𝐶 × 𝑥𝐴 𝐵) = 𝑥𝐴 (𝐶 × 𝐵)

Theoremxpiundir 4463* Distributive law for cross product over indexed union. (Contributed by Mario Carneiro, 27-Apr-2014.)
( 𝑥𝐴 𝐵 × 𝐶) = 𝑥𝐴 (𝐵 × 𝐶)

Theoremiunxpconst 4464* Membership in a union of cross products when the second factor is constant. (Contributed by Mario Carneiro, 29-Dec-2014.)
𝑥𝐴 ({𝑥} × 𝐵) = (𝐴 × 𝐵)

Theoremxpun 4465 The cross product of two unions. (Contributed by NM, 12-Aug-2004.)
((𝐴𝐵) × (𝐶𝐷)) = (((𝐴 × 𝐶) ∪ (𝐴 × 𝐷)) ∪ ((𝐵 × 𝐶) ∪ (𝐵 × 𝐷)))

Theoremelvv 4466* Membership in universal class of ordered pairs. (Contributed by NM, 4-Jul-1994.)
(𝐴 ∈ (V × V) ↔ ∃𝑥𝑦 𝐴 = ⟨𝑥, 𝑦⟩)

Theoremelvvv 4467* Membership in universal class of ordered triples. (Contributed by NM, 17-Dec-2008.)
(𝐴 ∈ ((V × V) × V) ↔ ∃𝑥𝑦𝑧 𝐴 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)

Theoremelvvuni 4468 An ordered pair contains its union. (Contributed by NM, 16-Sep-2006.)
(𝐴 ∈ (V × V) → 𝐴𝐴)

Theoremmosubopt 4469* "At most one" remains true inside ordered pair quantification. (Contributed by NM, 28-Aug-2007.)
(∀𝑦𝑧∃*𝑥𝜑 → ∃*𝑥𝑦𝑧(𝐴 = ⟨𝑦, 𝑧⟩ ∧ 𝜑))

Theoremmosubop 4470* "At most one" remains true inside ordered pair quantification. (Contributed by NM, 28-May-1995.)
∃*𝑥𝜑       ∃*𝑥𝑦𝑧(𝐴 = ⟨𝑦, 𝑧⟩ ∧ 𝜑)

Theorembrinxp2 4471 Intersection of binary relation with cross product. (Contributed by NM, 3-Mar-2007.) (Revised by Mario Carneiro, 26-Apr-2015.)
(𝐴(𝑅 ∩ (𝐶 × 𝐷))𝐵 ↔ (𝐴𝐶𝐵𝐷𝐴𝑅𝐵))

Theorembrinxp 4472 Intersection of binary relation with cross product. (Contributed by NM, 9-Mar-1997.)
((𝐴𝐶𝐵𝐷) → (𝐴𝑅𝐵𝐴(𝑅 ∩ (𝐶 × 𝐷))𝐵))

Theorempoinxp 4473 Intersection of partial order with cross product of its field. (Contributed by Mario Carneiro, 10-Jul-2014.)
(𝑅 Po 𝐴 ↔ (𝑅 ∩ (𝐴 × 𝐴)) Po 𝐴)

Theoremsoinxp 4474 Intersection of linear order with cross product of its field. (Contributed by Mario Carneiro, 10-Jul-2014.)
(𝑅 Or 𝐴 ↔ (𝑅 ∩ (𝐴 × 𝐴)) Or 𝐴)

Theoremseinxp 4475 Intersection of set-like relation with cross product of its field. (Contributed by Mario Carneiro, 22-Jun-2015.)
(𝑅 Se 𝐴 ↔ (𝑅 ∩ (𝐴 × 𝐴)) Se 𝐴)

Theoremposng 4476 Partial ordering of a singleton. (Contributed by Jim Kingdon, 5-Dec-2018.)
((Rel 𝑅𝐴 ∈ V) → (𝑅 Po {𝐴} ↔ ¬ 𝐴𝑅𝐴))

Theoremsosng 4477 Strict linear ordering on a singleton. (Contributed by Jim Kingdon, 5-Dec-2018.)
((Rel 𝑅𝐴 ∈ V) → (𝑅 Or {𝐴} ↔ ¬ 𝐴𝑅𝐴))

Theoremopabssxp 4478* An abstraction relation is a subset of a related cross product. (Contributed by NM, 16-Jul-1995.)
{⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝜑)} ⊆ (𝐴 × 𝐵)

Theorembrab2ga 4479* The law of concretion for a binary relation. See brab2a 4457 for alternate proof. TODO: should one of them be deleted? (Contributed by Mario Carneiro, 28-Apr-2015.) (Proof modification is discouraged.)
((𝑥 = 𝐴𝑦 = 𝐵) → (𝜑𝜓))    &   𝑅 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐶𝑦𝐷) ∧ 𝜑)}       (𝐴𝑅𝐵 ↔ ((𝐴𝐶𝐵𝐷) ∧ 𝜓))

Theoremoptocl 4480* Implicit substitution of class for ordered pair. (Contributed by NM, 5-Mar-1995.)
𝐷 = (𝐵 × 𝐶)    &   (⟨𝑥, 𝑦⟩ = 𝐴 → (𝜑𝜓))    &   ((𝑥𝐵𝑦𝐶) → 𝜑)       (𝐴𝐷𝜓)

Theorem2optocl 4481* Implicit substitution of classes for ordered pairs. (Contributed by NM, 12-Mar-1995.)
𝑅 = (𝐶 × 𝐷)    &   (⟨𝑥, 𝑦⟩ = 𝐴 → (𝜑𝜓))    &   (⟨𝑧, 𝑤⟩ = 𝐵 → (𝜓𝜒))    &   (((𝑥𝐶𝑦𝐷) ∧ (𝑧𝐶𝑤𝐷)) → 𝜑)       ((𝐴𝑅𝐵𝑅) → 𝜒)

Theorem3optocl 4482* Implicit substitution of classes for ordered pairs. (Contributed by NM, 12-Mar-1995.)
𝑅 = (𝐷 × 𝐹)    &   (⟨𝑥, 𝑦⟩ = 𝐴 → (𝜑𝜓))    &   (⟨𝑧, 𝑤⟩ = 𝐵 → (𝜓𝜒))    &   (⟨𝑣, 𝑢⟩ = 𝐶 → (𝜒𝜃))    &   (((𝑥𝐷𝑦𝐹) ∧ (𝑧𝐷𝑤𝐹) ∧ (𝑣𝐷𝑢𝐹)) → 𝜑)       ((𝐴𝑅𝐵𝑅𝐶𝑅) → 𝜃)

Theoremopbrop 4483* Ordered pair membership in a relation. Special case. (Contributed by NM, 5-Aug-1995.)
(((𝑧 = 𝐴𝑤 = 𝐵) ∧ (𝑣 = 𝐶𝑢 = 𝐷)) → (𝜑𝜓))    &   𝑅 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (𝑆 × 𝑆) ∧ 𝑦 ∈ (𝑆 × 𝑆)) ∧ ∃𝑧𝑤𝑣𝑢((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ 𝜑))}       (((𝐴𝑆𝐵𝑆) ∧ (𝐶𝑆𝐷𝑆)) → (⟨𝐴, 𝐵𝑅𝐶, 𝐷⟩ ↔ 𝜓))

Theorem0xp 4484 The cross product with the empty set is empty. Part of Theorem 3.13(ii) of [Monk1] p. 37. (Contributed by NM, 4-Jul-1994.)
(∅ × 𝐴) = ∅

Theoremcsbxpg 4485 Distribute proper substitution through the cross product of two classes. (Contributed by Alan Sare, 10-Nov-2012.)
(𝐴𝐷𝐴 / 𝑥(𝐵 × 𝐶) = (𝐴 / 𝑥𝐵 × 𝐴 / 𝑥𝐶))

Theoremreleq 4486 Equality theorem for the relation predicate. (Contributed by NM, 1-Aug-1994.)
(𝐴 = 𝐵 → (Rel 𝐴 ↔ Rel 𝐵))

Theoremreleqi 4487 Equality inference for the relation predicate. (Contributed by NM, 8-Dec-2006.)
𝐴 = 𝐵       (Rel 𝐴 ↔ Rel 𝐵)

Theoremreleqd 4488 Equality deduction for the relation predicate. (Contributed by NM, 8-Mar-2014.)
(𝜑𝐴 = 𝐵)       (𝜑 → (Rel 𝐴 ↔ Rel 𝐵))

Theoremnfrel 4489 Bound-variable hypothesis builder for a relation. (Contributed by NM, 31-Jan-2004.) (Revised by Mario Carneiro, 15-Oct-2016.)
𝑥𝐴       𝑥Rel 𝐴

Theoremsbcrel 4490 Distribute proper substitution through a relation predicate. (Contributed by Alexander van der Vekens, 23-Jul-2017.)
(𝐴𝑉 → ([𝐴 / 𝑥]Rel 𝑅 ↔ Rel 𝐴 / 𝑥𝑅))

Theoremrelss 4491 Subclass theorem for relation predicate. Theorem 2 of [Suppes] p. 58. (Contributed by NM, 15-Aug-1994.)
(𝐴𝐵 → (Rel 𝐵 → Rel 𝐴))

Theoremssrel 4492* A subclass relationship depends only on a relation's ordered pairs. Theorem 3.2(i) of [Monk1] p. 33. (Contributed by NM, 2-Aug-1994.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
(Rel 𝐴 → (𝐴𝐵 ↔ ∀𝑥𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵)))

Theoremeqrel 4493* Extensionality principle for relations. Theorem 3.2(ii) of [Monk1] p. 33. (Contributed by NM, 2-Aug-1994.)
((Rel 𝐴 ∧ Rel 𝐵) → (𝐴 = 𝐵 ↔ ∀𝑥𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐵)))

Theoremssrel2 4494* A subclass relationship depends only on a relation's ordered pairs. This version of ssrel 4492 is restricted to the relation's domain. (Contributed by Thierry Arnoux, 25-Jan-2018.)
(𝑅 ⊆ (𝐴 × 𝐵) → (𝑅𝑆 ↔ ∀𝑥𝐴𝑦𝐵 (⟨𝑥, 𝑦⟩ ∈ 𝑅 → ⟨𝑥, 𝑦⟩ ∈ 𝑆)))

Theoremrelssi 4495* Inference from subclass principle for relations. (Contributed by NM, 31-Mar-1998.)
Rel 𝐴    &   (⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵)       𝐴𝐵

Theoremrelssdv 4496* Deduction from subclass principle for relations. (Contributed by NM, 11-Sep-2004.)
(𝜑 → Rel 𝐴)    &   (𝜑 → (⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵))       (𝜑𝐴𝐵)

Theoremeqrelriv 4497* Inference from extensionality principle for relations. (Contributed by FL, 15-Oct-2012.)
(⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐵)       ((Rel 𝐴 ∧ Rel 𝐵) → 𝐴 = 𝐵)

Theoremeqrelriiv 4498* Inference from extensionality principle for relations. (Contributed by NM, 17-Mar-1995.)
Rel 𝐴    &   Rel 𝐵    &   (⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐵)       𝐴 = 𝐵

Theoremeqbrriv 4499* Inference from extensionality principle for relations. (Contributed by NM, 12-Dec-2006.)
Rel 𝐴    &   Rel 𝐵    &   (𝑥𝐴𝑦𝑥𝐵𝑦)       𝐴 = 𝐵

Theoremeqrelrdv 4500* Deduce equality of relations from equivalence of membership. (Contributed by Rodolfo Medina, 10-Oct-2010.)
Rel 𝐴    &   Rel 𝐵    &   (𝜑 → (⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐵))       (𝜑𝐴 = 𝐵)

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11354
 Copyright terms: Public domain < Previous  Next >
{"ft_lang_label":"__label__en","ft_lang_prob":0.68108374,"math_prob":0.90933365,"size":20536,"snap":"2022-40-2023-06","text_gpt3_token_len":10020,"char_repetition_ratio":0.21873173,"word_repetition_ratio":0.2821361,"special_character_ratio":0.4022205,"punctuation_ratio":0.13176711,"nsfw_num_words":0,"has_unicode_error":false,"math_prob_llama3":0.9717668,"pos_list":[0,1,2],"im_url_duplicate_count":[null,null,null],"WARC_HEADER":"{\"WARC-Type\":\"response\",\"WARC-Date\":\"2022-09-24T19:01:05Z\",\"WARC-Record-ID\":\"<urn:uuid:4756a811-599e-457e-b996-6c99fe593158>\",\"Content-Length\":\"138272\",\"Content-Type\":\"application/http; msgtype=response\",\"WARC-Warcinfo-ID\":\"<urn:uuid:c16b36aa-3cd9-48a4-8954-6b935f109424>\",\"WARC-Concurrent-To\":\"<urn:uuid:1520ef4c-46fe-4c70-b7cd-00934616bb81>\",\"WARC-IP-Address\":\"173.255.232.114\",\"WARC-Target-URI\":\"https://us.metamath.org/ileuni/mmtheorems45.html\",\"WARC-Payload-Digest\":\"sha1:YSLW7RF654EZRK73KZ6O3U4CHJIBJ2WB\",\"WARC-Block-Digest\":\"sha1:HOX3EJ6YMIMCZRRIWMEIARCX2MAWT4Z4\",\"WARC-Identified-Payload-Type\":\"text/html\",\"warc_filename\":\"/cc_download/warc_2022/CC-MAIN-2022-40/CC-MAIN-2022-40_segments_1664030333455.97_warc_CC-MAIN-20220924182740-20220924212740-00076.warc.gz\"}"}