Theorem List for Intuitionistic Logic Explorer - 5701-5800 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | oveq2i 5701 |
Equality inference for operation value. (Contributed by NM,
28-Feb-1995.)
|
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐶𝐹𝐴) = (𝐶𝐹𝐵) |
|
Theorem | oveq12i 5702 |
Equality inference for operation value. (Contributed by NM,
28-Feb-1995.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
|
⊢ 𝐴 = 𝐵
& ⊢ 𝐶 = 𝐷 ⇒ ⊢ (𝐴𝐹𝐶) = (𝐵𝐹𝐷) |
|
Theorem | oveqi 5703 |
Equality inference for operation value. (Contributed by NM,
24-Nov-2007.)
|
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐶𝐴𝐷) = (𝐶𝐵𝐷) |
|
Theorem | oveq123i 5704 |
Equality inference for operation value. (Contributed by FL,
11-Jul-2010.)
|
⊢ 𝐴 = 𝐶
& ⊢ 𝐵 = 𝐷
& ⊢ 𝐹 = 𝐺 ⇒ ⊢ (𝐴𝐹𝐵) = (𝐶𝐺𝐷) |
|
Theorem | oveq1d 5705 |
Equality deduction for operation value. (Contributed by NM,
13-Mar-1995.)
|
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶)) |
|
Theorem | oveq2d 5706 |
Equality deduction for operation value. (Contributed by NM,
13-Mar-1995.)
|
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵)) |
|
Theorem | oveqd 5707 |
Equality deduction for operation value. (Contributed by NM,
9-Sep-2006.)
|
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐶𝐴𝐷) = (𝐶𝐵𝐷)) |
|
Theorem | oveq12d 5708 |
Equality deduction for operation value. (Contributed by NM,
13-Mar-1995.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
|
⊢ (𝜑 → 𝐴 = 𝐵)
& ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝐴𝐹𝐶) = (𝐵𝐹𝐷)) |
|
Theorem | oveqan12d 5709 |
Equality deduction for operation value. (Contributed by NM,
10-Aug-1995.)
|
⊢ (𝜑 → 𝐴 = 𝐵)
& ⊢ (𝜓 → 𝐶 = 𝐷) ⇒ ⊢ ((𝜑 ∧ 𝜓) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷)) |
|
Theorem | oveqan12rd 5710 |
Equality deduction for operation value. (Contributed by NM,
10-Aug-1995.)
|
⊢ (𝜑 → 𝐴 = 𝐵)
& ⊢ (𝜓 → 𝐶 = 𝐷) ⇒ ⊢ ((𝜓 ∧ 𝜑) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷)) |
|
Theorem | oveq123d 5711 |
Equality deduction for operation value. (Contributed by FL,
22-Dec-2008.)
|
⊢ (𝜑 → 𝐹 = 𝐺)
& ⊢ (𝜑 → 𝐴 = 𝐵)
& ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝐴𝐹𝐶) = (𝐵𝐺𝐷)) |
|
Theorem | fvoveq1d 5712 |
Equality deduction for nested function and operation value.
(Contributed by AV, 23-Jul-2022.)
|
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐹‘(𝐴𝑂𝐶)) = (𝐹‘(𝐵𝑂𝐶))) |
|
Theorem | fvoveq1 5713 |
Equality theorem for nested function and operation value. Closed form of
fvoveq1d 5712. (Contributed by AV, 23-Jul-2022.)
|
⊢ (𝐴 = 𝐵 → (𝐹‘(𝐴𝑂𝐶)) = (𝐹‘(𝐵𝑂𝐶))) |
|
Theorem | ovanraleqv 5714* |
Equality theorem for a conjunction with an operation values within a
restricted universal quantification. Technical theorem to be used to
reduce the size of a significant number of proofs. (Contributed by AV,
13-Aug-2022.)
|
⊢ (𝐵 = 𝑋 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐵 = 𝑋 → (∀𝑥 ∈ 𝑉 (𝜑 ∧ (𝐴 · 𝐵) = 𝐶) ↔ ∀𝑥 ∈ 𝑉 (𝜓 ∧ (𝐴 · 𝑋) = 𝐶))) |
|
Theorem | imbrov2fvoveq 5715 |
Equality theorem for nested function and operation value in an
implication for a binary relation. Technical theorem to be used to
reduce the size of a significant number of proofs. (Contributed by AV,
17-Aug-2022.)
|
⊢ (𝑋 = 𝑌 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝑋 = 𝑌 → ((𝜑 → (𝐹‘((𝐺‘𝑋) · 𝑂))𝑅𝐴) ↔ (𝜓 → (𝐹‘((𝐺‘𝑌) · 𝑂))𝑅𝐴))) |
|
Theorem | nfovd 5716 |
Deduction version of bound-variable hypothesis builder nfov 5717.
(Contributed by NM, 13-Dec-2005.) (Proof shortened by Andrew Salmon,
22-Oct-2011.)
|
⊢ (𝜑 → Ⅎ𝑥𝐴)
& ⊢ (𝜑 → Ⅎ𝑥𝐹)
& ⊢ (𝜑 → Ⅎ𝑥𝐵) ⇒ ⊢ (𝜑 → Ⅎ𝑥(𝐴𝐹𝐵)) |
|
Theorem | nfov 5717 |
Bound-variable hypothesis builder for operation value. (Contributed by
NM, 4-May-2004.)
|
⊢ Ⅎ𝑥𝐴
& ⊢ Ⅎ𝑥𝐹
& ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥(𝐴𝐹𝐵) |
|
Theorem | oprabidlem 5718* |
Slight elaboration of exdistrfor 1735. A lemma for oprabid 5719.
(Contributed by Jim Kingdon, 15-Jan-2019.)
|
⊢ (∃𝑥∃𝑦(𝑥 = 𝑧 ∧ 𝜓) → ∃𝑥(𝑥 = 𝑧 ∧ ∃𝑦𝜓)) |
|
Theorem | oprabid 5719 |
The law of concretion. Special case of Theorem 9.5 of [Quine] p. 61.
Although this theorem would be useful with a distinct variable
constraint between 𝑥, 𝑦, and 𝑧, we use ax-bndl 1451 to
eliminate that constraint. (Contributed by Mario Carneiro,
20-Mar-2013.)
|
⊢ (〈〈𝑥, 𝑦〉, 𝑧〉 ∈ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} ↔ 𝜑) |
|
Theorem | fnovex 5720 |
The result of an operation is a set. (Contributed by Jim Kingdon,
15-Jan-2019.)
|
⊢ ((𝐹 Fn (𝐶 × 𝐷) ∧ 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴𝐹𝐵) ∈ V) |
|
Theorem | ovexg 5721 |
Evaluating a set operation at two sets gives a set. (Contributed by Jim
Kingdon, 19-Aug-2021.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 ∈ 𝑊 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐹𝐵) ∈ V) |
|
Theorem | ovprc 5722 |
The value of an operation when the one of the arguments is a proper
class. Note: this theorem is dependent on our particular definitions of
operation value, function value, and ordered pair. (Contributed by
Mario Carneiro, 26-Apr-2015.)
|
⊢ Rel dom 𝐹 ⇒ ⊢ (¬ (𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴𝐹𝐵) = ∅) |
|
Theorem | ovprc1 5723 |
The value of an operation when the first argument is a proper class.
(Contributed by NM, 16-Jun-2004.)
|
⊢ Rel dom 𝐹 ⇒ ⊢ (¬ 𝐴 ∈ V → (𝐴𝐹𝐵) = ∅) |
|
Theorem | ovprc2 5724 |
The value of an operation when the second argument is a proper class.
(Contributed by Mario Carneiro, 26-Apr-2015.)
|
⊢ Rel dom 𝐹 ⇒ ⊢ (¬ 𝐵 ∈ V → (𝐴𝐹𝐵) = ∅) |
|
Theorem | csbov123g 5725 |
Move class substitution in and out of an operation. (Contributed by NM,
12-Nov-2005.) (Proof shortened by Mario Carneiro, 5-Dec-2016.)
|
⊢ (𝐴 ∈ 𝐷 → ⦋𝐴 / 𝑥⦌(𝐵𝐹𝐶) = (⦋𝐴 / 𝑥⦌𝐵⦋𝐴 / 𝑥⦌𝐹⦋𝐴 / 𝑥⦌𝐶)) |
|
Theorem | csbov12g 5726* |
Move class substitution in and out of an operation. (Contributed by NM,
12-Nov-2005.)
|
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(𝐵𝐹𝐶) = (⦋𝐴 / 𝑥⦌𝐵𝐹⦋𝐴 / 𝑥⦌𝐶)) |
|
Theorem | csbov1g 5727* |
Move class substitution in and out of an operation. (Contributed by NM,
12-Nov-2005.)
|
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(𝐵𝐹𝐶) = (⦋𝐴 / 𝑥⦌𝐵𝐹𝐶)) |
|
Theorem | csbov2g 5728* |
Move class substitution in and out of an operation. (Contributed by NM,
12-Nov-2005.)
|
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(𝐵𝐹𝐶) = (𝐵𝐹⦋𝐴 / 𝑥⦌𝐶)) |
|
Theorem | rspceov 5729* |
A frequently used special case of rspc2ev 2750 for operation values.
(Contributed by NM, 21-Mar-2007.)
|
⊢ ((𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ∧ 𝑆 = (𝐶𝐹𝐷)) → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑆 = (𝑥𝐹𝑦)) |
|
Theorem | fnotovb 5730 |
Equivalence of operation value and ordered triple membership, analogous to
fnopfvb 5381. (Contributed by NM, 17-Dec-2008.) (Revised
by Mario
Carneiro, 28-Apr-2015.)
|
⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵) → ((𝐶𝐹𝐷) = 𝑅 ↔ 〈𝐶, 𝐷, 𝑅〉 ∈ 𝐹)) |
|
Theorem | opabbrex 5731* |
A collection of ordered pairs with an extension of a binary relation is
a set. (Contributed by Alexander van der Vekens, 1-Nov-2017.)
|
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑓(𝑉𝑊𝐸)𝑝 → 𝜃)) & ⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → {〈𝑓, 𝑝〉 ∣ 𝜃} ∈ V) ⇒ ⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → {〈𝑓, 𝑝〉 ∣ (𝑓(𝑉𝑊𝐸)𝑝 ∧ 𝜓)} ∈ V) |
|
Theorem | 0neqopab 5732 |
The empty set is never an element in an ordered-pair class abstraction.
(Contributed by Alexander van der Vekens, 5-Nov-2017.)
|
⊢ ¬ ∅ ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} |
|
Theorem | brabvv 5733* |
If two classes are in a relationship given by an ordered-pair class
abstraction, the classes are sets. (Contributed by Jim Kingdon,
16-Jan-2019.)
|
⊢ (𝑋{〈𝑥, 𝑦〉 ∣ 𝜑}𝑌 → (𝑋 ∈ V ∧ 𝑌 ∈ V)) |
|
Theorem | dfoprab2 5734* |
Class abstraction for operations in terms of class abstraction of
ordered pairs. (Contributed by NM, 12-Mar-1995.)
|
⊢ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} = {〈𝑤, 𝑧〉 ∣ ∃𝑥∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝜑)} |
|
Theorem | reloprab 5735* |
An operation class abstraction is a relation. (Contributed by NM,
16-Jun-2004.)
|
⊢ Rel {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} |
|
Theorem | nfoprab1 5736 |
The abstraction variables in an operation class abstraction are not
free. (Contributed by NM, 25-Apr-1995.) (Revised by David Abernethy,
19-Jun-2012.)
|
⊢ Ⅎ𝑥{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} |
|
Theorem | nfoprab2 5737 |
The abstraction variables in an operation class abstraction are not
free. (Contributed by NM, 25-Apr-1995.) (Revised by David Abernethy,
30-Jul-2012.)
|
⊢ Ⅎ𝑦{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} |
|
Theorem | nfoprab3 5738 |
The abstraction variables in an operation class abstraction are not
free. (Contributed by NM, 22-Aug-2013.)
|
⊢ Ⅎ𝑧{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} |
|
Theorem | nfoprab 5739* |
Bound-variable hypothesis builder for an operation class abstraction.
(Contributed by NM, 22-Aug-2013.)
|
⊢ Ⅎ𝑤𝜑 ⇒ ⊢ Ⅎ𝑤{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} |
|
Theorem | oprabbid 5740* |
Equivalent wff's yield equal operation class abstractions (deduction
form). (Contributed by NM, 21-Feb-2004.) (Revised by Mario Carneiro,
24-Jun-2014.)
|
⊢ Ⅎ𝑥𝜑
& ⊢ Ⅎ𝑦𝜑
& ⊢ Ⅎ𝑧𝜑
& ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜓} = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜒}) |
|
Theorem | oprabbidv 5741* |
Equivalent wff's yield equal operation class abstractions (deduction
form). (Contributed by NM, 21-Feb-2004.)
|
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜓} = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜒}) |
|
Theorem | oprabbii 5742* |
Equivalent wff's yield equal operation class abstractions. (Contributed
by NM, 28-May-1995.) (Revised by David Abernethy, 19-Jun-2012.)
|
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜓} |
|
Theorem | ssoprab2 5743 |
Equivalence of ordered pair abstraction subclass and implication.
Compare ssopab2 4126. (Contributed by FL, 6-Nov-2013.) (Proof
shortened
by Mario Carneiro, 11-Dec-2016.)
|
⊢ (∀𝑥∀𝑦∀𝑧(𝜑 → 𝜓) → {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} ⊆ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜓}) |
|
Theorem | ssoprab2b 5744 |
Equivalence of ordered pair abstraction subclass and implication. Compare
ssopab2b 4127. (Contributed by FL, 6-Nov-2013.) (Proof
shortened by Mario
Carneiro, 11-Dec-2016.)
|
⊢ ({〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} ⊆ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜓} ↔ ∀𝑥∀𝑦∀𝑧(𝜑 → 𝜓)) |
|
Theorem | eqoprab2b 5745 |
Equivalence of ordered pair abstraction subclass and biconditional.
Compare eqopab2b 4130. (Contributed by Mario Carneiro,
4-Jan-2017.)
|
⊢ ({〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜓} ↔ ∀𝑥∀𝑦∀𝑧(𝜑 ↔ 𝜓)) |
|
Theorem | mpt2eq123 5746* |
An equality theorem for the maps-to notation. (Contributed by Mario
Carneiro, 16-Dec-2013.) (Revised by Mario Carneiro, 19-Mar-2015.)
|
⊢ ((𝐴 = 𝐷 ∧ ∀𝑥 ∈ 𝐴 (𝐵 = 𝐸 ∧ ∀𝑦 ∈ 𝐵 𝐶 = 𝐹)) → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐷, 𝑦 ∈ 𝐸 ↦ 𝐹)) |
|
Theorem | mpt2eq12 5747* |
An equality theorem for the maps-to notation. (Contributed by Mario
Carneiro, 16-Dec-2013.)
|
⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐸) = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝐸)) |
|
Theorem | mpt2eq123dva 5748* |
An equality deduction for the maps-to notation. (Contributed by Mario
Carneiro, 26-Jan-2017.)
|
⊢ (𝜑 → 𝐴 = 𝐷)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐸)
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝐶 = 𝐹) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐷, 𝑦 ∈ 𝐸 ↦ 𝐹)) |
|
Theorem | mpt2eq123dv 5749* |
An equality deduction for the maps-to notation. (Contributed by NM,
12-Sep-2011.)
|
⊢ (𝜑 → 𝐴 = 𝐷)
& ⊢ (𝜑 → 𝐵 = 𝐸)
& ⊢ (𝜑 → 𝐶 = 𝐹) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐷, 𝑦 ∈ 𝐸 ↦ 𝐹)) |
|
Theorem | mpt2eq123i 5750 |
An equality inference for the maps-to notation. (Contributed by NM,
15-Jul-2013.)
|
⊢ 𝐴 = 𝐷
& ⊢ 𝐵 = 𝐸
& ⊢ 𝐶 = 𝐹 ⇒ ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐷, 𝑦 ∈ 𝐸 ↦ 𝐹) |
|
Theorem | mpt2eq3dva 5751* |
Slightly more general equality inference for the maps-to notation.
(Contributed by NM, 17-Oct-2013.)
|
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷)) |
|
Theorem | mpt2eq3ia 5752 |
An equality inference for the maps-to notation. (Contributed by Mario
Carneiro, 16-Dec-2013.)
|
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐶 = 𝐷) ⇒ ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷) |
|
Theorem | nfmpt21 5753 |
Bound-variable hypothesis builder for an operation in maps-to notation.
(Contributed by NM, 27-Aug-2013.)
|
⊢ Ⅎ𝑥(𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) |
|
Theorem | nfmpt22 5754 |
Bound-variable hypothesis builder for an operation in maps-to notation.
(Contributed by NM, 27-Aug-2013.)
|
⊢ Ⅎ𝑦(𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) |
|
Theorem | nfmpt2 5755* |
Bound-variable hypothesis builder for the maps-to notation.
(Contributed by NM, 20-Feb-2013.)
|
⊢ Ⅎ𝑧𝐴
& ⊢ Ⅎ𝑧𝐵
& ⊢ Ⅎ𝑧𝐶 ⇒ ⊢ Ⅎ𝑧(𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) |
|
Theorem | mpt20 5756 |
A mapping operation with empty domain. (Contributed by Stefan O'Rear,
29-Jan-2015.) (Revised by Mario Carneiro, 15-May-2015.)
|
⊢ (𝑥 ∈ ∅, 𝑦 ∈ 𝐵 ↦ 𝐶) = ∅ |
|
Theorem | oprab4 5757* |
Two ways to state the domain of an operation. (Contributed by FL,
24-Jan-2010.)
|
⊢ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ (〈𝑥, 𝑦〉 ∈ (𝐴 × 𝐵) ∧ 𝜑)} = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)} |
|
Theorem | cbvoprab1 5758* |
Rule used to change first bound variable in an operation abstraction,
using implicit substitution. (Contributed by NM, 20-Dec-2008.)
(Revised by Mario Carneiro, 5-Dec-2016.)
|
⊢ Ⅎ𝑤𝜑
& ⊢ Ⅎ𝑥𝜓
& ⊢ (𝑥 = 𝑤 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} = {〈〈𝑤, 𝑦〉, 𝑧〉 ∣ 𝜓} |
|
Theorem | cbvoprab2 5759* |
Change the second bound variable in an operation abstraction.
(Contributed by Jeff Madsen, 11-Jun-2010.) (Revised by Mario Carneiro,
11-Dec-2016.)
|
⊢ Ⅎ𝑤𝜑
& ⊢ Ⅎ𝑦𝜓
& ⊢ (𝑦 = 𝑤 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} = {〈〈𝑥, 𝑤〉, 𝑧〉 ∣ 𝜓} |
|
Theorem | cbvoprab12 5760* |
Rule used to change first two bound variables in an operation
abstraction, using implicit substitution. (Contributed by NM,
21-Feb-2004.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
|
⊢ Ⅎ𝑤𝜑
& ⊢ Ⅎ𝑣𝜑
& ⊢ Ⅎ𝑥𝜓
& ⊢ Ⅎ𝑦𝜓
& ⊢ ((𝑥 = 𝑤 ∧ 𝑦 = 𝑣) → (𝜑 ↔ 𝜓)) ⇒ ⊢ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} = {〈〈𝑤, 𝑣〉, 𝑧〉 ∣ 𝜓} |
|
Theorem | cbvoprab12v 5761* |
Rule used to change first two bound variables in an operation
abstraction, using implicit substitution. (Contributed by NM,
8-Oct-2004.)
|
⊢ ((𝑥 = 𝑤 ∧ 𝑦 = 𝑣) → (𝜑 ↔ 𝜓)) ⇒ ⊢ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} = {〈〈𝑤, 𝑣〉, 𝑧〉 ∣ 𝜓} |
|
Theorem | cbvoprab3 5762* |
Rule used to change the third bound variable in an operation
abstraction, using implicit substitution. (Contributed by NM,
22-Aug-2013.)
|
⊢ Ⅎ𝑤𝜑
& ⊢ Ⅎ𝑧𝜓
& ⊢ (𝑧 = 𝑤 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} = {〈〈𝑥, 𝑦〉, 𝑤〉 ∣ 𝜓} |
|
Theorem | cbvoprab3v 5763* |
Rule used to change the third bound variable in an operation
abstraction, using implicit substitution. (Contributed by NM,
8-Oct-2004.) (Revised by David Abernethy, 19-Jun-2012.)
|
⊢ (𝑧 = 𝑤 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} = {〈〈𝑥, 𝑦〉, 𝑤〉 ∣ 𝜓} |
|
Theorem | cbvmpt2x 5764* |
Rule to change the bound variable in a maps-to function, using implicit
substitution. This version of cbvmpt2 5765 allows 𝐵 to be a function
of 𝑥. (Contributed by NM, 29-Dec-2014.)
|
⊢ Ⅎ𝑧𝐵
& ⊢ Ⅎ𝑥𝐷
& ⊢ Ⅎ𝑧𝐶
& ⊢ Ⅎ𝑤𝐶
& ⊢ Ⅎ𝑥𝐸
& ⊢ Ⅎ𝑦𝐸
& ⊢ (𝑥 = 𝑧 → 𝐵 = 𝐷)
& ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝐶 = 𝐸) ⇒ ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑧 ∈ 𝐴, 𝑤 ∈ 𝐷 ↦ 𝐸) |
|
Theorem | cbvmpt2 5765* |
Rule to change the bound variable in a maps-to function, using implicit
substitution. (Contributed by NM, 17-Dec-2013.)
|
⊢ Ⅎ𝑧𝐶
& ⊢ Ⅎ𝑤𝐶
& ⊢ Ⅎ𝑥𝐷
& ⊢ Ⅎ𝑦𝐷
& ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝐶 = 𝐷) ⇒ ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑧 ∈ 𝐴, 𝑤 ∈ 𝐵 ↦ 𝐷) |
|
Theorem | cbvmpt2v 5766* |
Rule to change the bound variable in a maps-to function, using implicit
substitution. With a longer proof analogous to cbvmpt 3955, some distinct
variable requirements could be eliminated. (Contributed by NM,
11-Jun-2013.)
|
⊢ (𝑥 = 𝑧 → 𝐶 = 𝐸)
& ⊢ (𝑦 = 𝑤 → 𝐸 = 𝐷) ⇒ ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑧 ∈ 𝐴, 𝑤 ∈ 𝐵 ↦ 𝐷) |
|
Theorem | dmoprab 5767* |
The domain of an operation class abstraction. (Contributed by NM,
17-Mar-1995.) (Revised by David Abernethy, 19-Jun-2012.)
|
⊢ dom {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} = {〈𝑥, 𝑦〉 ∣ ∃𝑧𝜑} |
|
Theorem | dmoprabss 5768* |
The domain of an operation class abstraction. (Contributed by NM,
24-Aug-1995.)
|
⊢ dom {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)} ⊆ (𝐴 × 𝐵) |
|
Theorem | rnoprab 5769* |
The range of an operation class abstraction. (Contributed by NM,
30-Aug-2004.) (Revised by David Abernethy, 19-Apr-2013.)
|
⊢ ran {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} = {𝑧 ∣ ∃𝑥∃𝑦𝜑} |
|
Theorem | rnoprab2 5770* |
The range of a restricted operation class abstraction. (Contributed by
Scott Fenton, 21-Mar-2012.)
|
⊢ ran {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)} = {𝑧 ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑} |
|
Theorem | reldmoprab 5771* |
The domain of an operation class abstraction is a relation.
(Contributed by NM, 17-Mar-1995.)
|
⊢ Rel dom {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} |
|
Theorem | oprabss 5772* |
Structure of an operation class abstraction. (Contributed by NM,
28-Nov-2006.)
|
⊢ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} ⊆ ((V × V) ×
V) |
|
Theorem | eloprabga 5773* |
The law of concretion for operation class abstraction. Compare
elopab 4109. (Contributed by NM, 14-Sep-1999.)
(Unnecessary distinct
variable restrictions were removed by David Abernethy, 19-Jun-2012.)
(Revised by Mario Carneiro, 19-Dec-2013.)
|
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (〈〈𝐴, 𝐵〉, 𝐶〉 ∈ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} ↔ 𝜓)) |
|
Theorem | eloprabg 5774* |
The law of concretion for operation class abstraction. Compare
elopab 4109. (Contributed by NM, 14-Sep-1999.) (Revised
by David
Abernethy, 19-Jun-2012.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ (𝑧 = 𝐶 → (𝜒 ↔ 𝜃)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (〈〈𝐴, 𝐵〉, 𝐶〉 ∈ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} ↔ 𝜃)) |
|
Theorem | ssoprab2i 5775* |
Inference of operation class abstraction subclass from implication.
(Contributed by NM, 11-Nov-1995.) (Revised by David Abernethy,
19-Jun-2012.)
|
⊢ (𝜑 → 𝜓) ⇒ ⊢ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} ⊆ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜓} |
|
Theorem | mpt2v 5776* |
Operation with universal domain in maps-to notation. (Contributed by
NM, 16-Aug-2013.)
|
⊢ (𝑥 ∈ V, 𝑦 ∈ V ↦ 𝐶) = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝑧 = 𝐶} |
|
Theorem | mpt2mptx 5777* |
Express a two-argument function as a one-argument function, or
vice-versa. In this version 𝐵(𝑥) is not assumed to be constant
w.r.t 𝑥. (Contributed by Mario Carneiro,
29-Dec-2014.)
|
⊢ (𝑧 = 〈𝑥, 𝑦〉 → 𝐶 = 𝐷) ⇒ ⊢ (𝑧 ∈ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷) |
|
Theorem | mpt2mpt 5778* |
Express a two-argument function as a one-argument function, or
vice-versa. (Contributed by Mario Carneiro, 17-Dec-2013.) (Revised by
Mario Carneiro, 29-Dec-2014.)
|
⊢ (𝑧 = 〈𝑥, 𝑦〉 → 𝐶 = 𝐷) ⇒ ⊢ (𝑧 ∈ (𝐴 × 𝐵) ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷) |
|
Theorem | resoprab 5779* |
Restriction of an operation class abstraction. (Contributed by NM,
10-Feb-2007.)
|
⊢ ({〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} ↾ (𝐴 × 𝐵)) = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)} |
|
Theorem | resoprab2 5780* |
Restriction of an operator abstraction. (Contributed by Jeff Madsen,
2-Sep-2009.)
|
⊢ ((𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐵) → ({〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)} ↾ (𝐶 × 𝐷)) = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) ∧ 𝜑)}) |
|
Theorem | resmpt2 5781* |
Restriction of the mapping operation. (Contributed by Mario Carneiro,
17-Dec-2013.)
|
⊢ ((𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐵) → ((𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐸) ↾ (𝐶 × 𝐷)) = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝐸)) |
|
Theorem | funoprabg 5782* |
"At most one" is a sufficient condition for an operation class
abstraction to be a function. (Contributed by NM, 28-Aug-2007.)
|
⊢ (∀𝑥∀𝑦∃*𝑧𝜑 → Fun {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑}) |
|
Theorem | funoprab 5783* |
"At most one" is a sufficient condition for an operation class
abstraction to be a function. (Contributed by NM, 17-Mar-1995.)
|
⊢ ∃*𝑧𝜑 ⇒ ⊢ Fun {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} |
|
Theorem | fnoprabg 5784* |
Functionality and domain of an operation class abstraction.
(Contributed by NM, 28-Aug-2007.)
|
⊢ (∀𝑥∀𝑦(𝜑 → ∃!𝑧𝜓) → {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ (𝜑 ∧ 𝜓)} Fn {〈𝑥, 𝑦〉 ∣ 𝜑}) |
|
Theorem | mpt2fun 5785* |
The maps-to notation for an operation is always a function.
(Contributed by Scott Fenton, 21-Mar-2012.)
|
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ⇒ ⊢ Fun 𝐹 |
|
Theorem | fnoprab 5786* |
Functionality and domain of an operation class abstraction.
(Contributed by NM, 15-May-1995.)
|
⊢ (𝜑 → ∃!𝑧𝜓) ⇒ ⊢ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ (𝜑 ∧ 𝜓)} Fn {〈𝑥, 𝑦〉 ∣ 𝜑} |
|
Theorem | ffnov 5787* |
An operation maps to a class to which all values belong. (Contributed
by NM, 7-Feb-2004.)
|
⊢ (𝐹:(𝐴 × 𝐵)⟶𝐶 ↔ (𝐹 Fn (𝐴 × 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥𝐹𝑦) ∈ 𝐶)) |
|
Theorem | fovcl 5788 |
Closure law for an operation. (Contributed by NM, 19-Apr-2007.)
|
⊢ 𝐹:(𝑅 × 𝑆)⟶𝐶 ⇒ ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → (𝐴𝐹𝐵) ∈ 𝐶) |
|
Theorem | eqfnov 5789* |
Equality of two operations is determined by their values. (Contributed
by NM, 1-Sep-2005.)
|
⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐺 Fn (𝐶 × 𝐷)) → (𝐹 = 𝐺 ↔ ((𝐴 × 𝐵) = (𝐶 × 𝐷) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥𝐹𝑦) = (𝑥𝐺𝑦)))) |
|
Theorem | eqfnov2 5790* |
Two operators with the same domain are equal iff their values at each
point in the domain are equal. (Contributed by Jeff Madsen,
7-Jun-2010.)
|
⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐺 Fn (𝐴 × 𝐵)) → (𝐹 = 𝐺 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥𝐹𝑦) = (𝑥𝐺𝑦))) |
|
Theorem | fnovim 5791* |
Representation of a function in terms of its values. (Contributed by
Jim Kingdon, 16-Jan-2019.)
|
⊢ (𝐹 Fn (𝐴 × 𝐵) → 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ (𝑥𝐹𝑦))) |
|
Theorem | mpt22eqb 5792* |
Bidirectional equality theorem for a mapping abstraction. Equivalent to
eqfnov2 5790. (Contributed by Mario Carneiro,
4-Jan-2017.)
|
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝑉 → ((𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 = 𝐷)) |
|
Theorem | rnmpt2 5793* |
The range of an operation given by the maps-to notation. (Contributed
by FL, 20-Jun-2011.)
|
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ⇒ ⊢ ran 𝐹 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = 𝐶} |
|
Theorem | reldmmpt2 5794* |
The domain of an operation defined by maps-to notation is a relation.
(Contributed by Stefan O'Rear, 27-Nov-2014.)
|
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ⇒ ⊢ Rel dom 𝐹 |
|
Theorem | elrnmpt2g 5795* |
Membership in the range of an operation class abstraction. (Contributed
by NM, 27-Aug-2007.) (Revised by Mario Carneiro, 31-Aug-2015.)
|
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ⇒ ⊢ (𝐷 ∈ 𝑉 → (𝐷 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝐷 = 𝐶)) |
|
Theorem | elrnmpt2 5796* |
Membership in the range of an operation class abstraction.
(Contributed by NM, 1-Aug-2004.) (Revised by Mario Carneiro,
31-Aug-2015.)
|
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
& ⊢ 𝐶 ∈ V ⇒ ⊢ (𝐷 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝐷 = 𝐶) |
|
Theorem | ralrnmpt2 5797* |
A restricted quantifier over an image set. (Contributed by Mario
Carneiro, 1-Sep-2015.)
|
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
& ⊢ (𝑧 = 𝐶 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝑉 → (∀𝑧 ∈ ran 𝐹𝜑 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓)) |
|
Theorem | rexrnmpt2 5798* |
A restricted quantifier over an image set. (Contributed by Mario
Carneiro, 1-Sep-2015.)
|
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
& ⊢ (𝑧 = 𝐶 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝑉 → (∃𝑧 ∈ ran 𝐹𝜑 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓)) |
|
Theorem | ovid 5799* |
The value of an operation class abstraction. (Contributed by NM,
16-May-1995.) (Revised by David Abernethy, 19-Jun-2012.)
|
⊢ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) → ∃!𝑧𝜑)
& ⊢ 𝐹 = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) ∧ 𝜑)} ⇒ ⊢ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) → ((𝑥𝐹𝑦) = 𝑧 ↔ 𝜑)) |
|
Theorem | ovidig 5800* |
The value of an operation class abstraction. Compare ovidi 5801. The
condition (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) is been removed. (Contributed by
Mario Carneiro, 29-Dec-2014.)
|
⊢ ∃*𝑧𝜑
& ⊢ 𝐹 = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} ⇒ ⊢ (𝜑 → (𝑥𝐹𝑦) = 𝑧) |