P. 56 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 5501-5600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	riotauni 5501	Restricted iota in terms of class union. (Contributed by NM, 11-Oct-2011.)
⊢ (∃!𝑥 ∈ 𝐴 𝜑 → (℩𝑥 ∈ 𝐴 𝜑) = ∪ {𝑥 ∈ 𝐴 ∣ 𝜑})
Theorem	nfriota1 5502*	The abstraction variable in a restricted iota descriptor isn't free. (Contributed by NM, 12-Oct-2011.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ Ⅎ𝑥(℩𝑥 ∈ 𝐴 𝜑)
Theorem	nfriotadxy 5503*	Deduction version of nfriota 5504. (Contributed by Jim Kingdon, 12-Jan-2019.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    &   ⊢ (𝜑 → Ⅎ𝑥𝐴)    ⇒   ⊢ (𝜑 → Ⅎ𝑥(℩𝑦 ∈ 𝐴 𝜓))
Theorem	nfriota 5504*	A variable not free in a wff remains so in a restricted iota descriptor. (Contributed by NM, 12-Oct-2011.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥(℩𝑦 ∈ 𝐴 𝜑)
Theorem	cbvriota 5505*	Change bound variable in a restricted description binder. (Contributed by NM, 18-Mar-2013.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑦 ∈ 𝐴 𝜓)
Theorem	cbvriotav 5506*	Change bound variable in a restricted description binder. (Contributed by NM, 18-Mar-2013.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑦 ∈ 𝐴 𝜓)
Theorem	csbriotag 5507*	Interchange class substitution and restricted description binder. (Contributed by NM, 24-Feb-2013.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(℩𝑦 ∈ 𝐵 𝜑) = (℩𝑦 ∈ 𝐵 [𝐴 / 𝑥]𝜑))
Theorem	riotacl2 5508	Membership law for "the unique element in 𝐴 such that 𝜑." (Contributed by NM, 21-Aug-2011.) (Revised by Mario Carneiro, 23-Dec-2016.)
⊢ (∃!𝑥 ∈ 𝐴 𝜑 → (℩𝑥 ∈ 𝐴 𝜑) ∈ {𝑥 ∈ 𝐴 ∣ 𝜑})
Theorem	riotacl 5509*	Closure of restricted iota. (Contributed by NM, 21-Aug-2011.)
⊢ (∃!𝑥 ∈ 𝐴 𝜑 → (℩𝑥 ∈ 𝐴 𝜑) ∈ 𝐴)
Theorem	riotasbc 5510	Substitution law for descriptions. (Contributed by NM, 23-Aug-2011.) (Proof shortened by Mario Carneiro, 24-Dec-2016.)
⊢ (∃!𝑥 ∈ 𝐴 𝜑 → [(℩𝑥 ∈ 𝐴 𝜑) / 𝑥]𝜑)
Theorem	riotabidva 5511*	Equivalent wff's yield equal restricted class abstractions (deduction rule). (rabbidva 2565 analog.) (Contributed by NM, 17-Jan-2012.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = (℩𝑥 ∈ 𝐴 𝜒))
Theorem	riotabiia 5512	Equivalent wff's yield equal restricted iotas (inference rule). (rabbiia 2564 analog.) (Contributed by NM, 16-Jan-2012.)
⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥 ∈ 𝐴 𝜓)
Theorem	riota1 5513*	Property of restricted iota. Compare iota1 4908. (Contributed by Mario Carneiro, 15-Oct-2016.)
⊢ (∃!𝑥 ∈ 𝐴 𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (℩𝑥 ∈ 𝐴 𝜑) = 𝑥))
Theorem	riota1a 5514	Property of iota. (Contributed by NM, 23-Aug-2011.)
⊢ ((𝑥 ∈ 𝐴 ∧ ∃!𝑥 ∈ 𝐴 𝜑) → (𝜑 ↔ (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) = 𝑥))
Theorem	riota2df 5515*	A deduction version of riota2f 5516. (Contributed by NM, 17-Feb-2013.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝐵)    &   ⊢ (𝜑 → Ⅎ𝑥𝜒)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐵) → (𝜓 ↔ 𝜒))    ⇒   ⊢ ((𝜑 ∧ ∃!𝑥 ∈ 𝐴 𝜓) → (𝜒 ↔ (℩𝑥 ∈ 𝐴 𝜓) = 𝐵))
Theorem	riota2f 5516*	This theorem shows a condition that allows us to represent a descriptor with a class expression 𝐵. (Contributed by NM, 23-Aug-2011.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ Ⅎ𝑥𝐵    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝐵 ∈ 𝐴 ∧ ∃!𝑥 ∈ 𝐴 𝜑) → (𝜓 ↔ (℩𝑥 ∈ 𝐴 𝜑) = 𝐵))
Theorem	riota2 5517*	This theorem shows a condition that allows us to represent a descriptor with a class expression 𝐵. (Contributed by NM, 23-Aug-2011.) (Revised by Mario Carneiro, 10-Dec-2016.)
⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝐵 ∈ 𝐴 ∧ ∃!𝑥 ∈ 𝐴 𝜑) → (𝜓 ↔ (℩𝑥 ∈ 𝐴 𝜑) = 𝐵))
Theorem	riotaprop 5518*	Properties of a restricted definite description operator. Todo (df-riota 5495 update): can some uses of riota2f 5516 be shortened with this? (Contributed by NM, 23-Nov-2013.)
⊢ Ⅎ𝑥𝜓    &   ⊢ 𝐵 = (℩𝑥 ∈ 𝐴 𝜑)    &   ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃!𝑥 ∈ 𝐴 𝜑 → (𝐵 ∈ 𝐴 ∧ 𝜓))
Theorem	riota5f 5519*	A method for computing restricted iota. (Contributed by NM, 16-Apr-2013.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ (𝜑 → Ⅎ𝑥𝐵)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝑥 = 𝐵))    ⇒   ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = 𝐵)
Theorem	riota5 5520*	A method for computing restricted iota. (Contributed by NM, 20-Oct-2011.) (Revised by Mario Carneiro, 6-Dec-2016.)
⊢ (𝜑 → 𝐵 ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝑥 = 𝐵))    ⇒   ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = 𝐵)
Theorem	riotass2 5521*	Restriction of a unique element to a smaller class. (Contributed by NM, 21-Aug-2011.) (Revised by NM, 22-Mar-2013.)
⊢ (((𝐴 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓)) ∧ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃!𝑥 ∈ 𝐵 𝜓)) → (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥 ∈ 𝐵 𝜓))
Theorem	riotass 5522*	Restriction of a unique element to a smaller class. (Contributed by NM, 19-Oct-2005.) (Revised by Mario Carneiro, 24-Dec-2016.)
⊢ ((𝐴 ⊆ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝜑 ∧ ∃!𝑥 ∈ 𝐵 𝜑) → (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥 ∈ 𝐵 𝜑))
Theorem	moriotass 5523*	Restriction of a unique element to a smaller class. (Contributed by NM, 19-Feb-2006.) (Revised by NM, 16-Jun-2017.)
⊢ ((𝐴 ⊆ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐵 𝜑) → (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥 ∈ 𝐵 𝜑))
Theorem	snriota 5524	A restricted class abstraction with a unique member can be expressed as a singleton. (Contributed by NM, 30-May-2006.)
⊢ (∃!𝑥 ∈ 𝐴 𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜑} = {(℩𝑥 ∈ 𝐴 𝜑)})
Theorem	eusvobj2 5525*	Specify the same property in two ways when class 𝐵(𝑦) is single-valued. (Contributed by NM, 1-Nov-2010.) (Proof shortened by Mario Carneiro, 24-Dec-2016.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (∃!𝑥∃𝑦 ∈ 𝐴 𝑥 = 𝐵 → (∃𝑦 ∈ 𝐴 𝑥 = 𝐵 ↔ ∀𝑦 ∈ 𝐴 𝑥 = 𝐵))
Theorem	eusvobj1 5526*	Specify the same object in two ways when class 𝐵(𝑦) is single-valued. (Contributed by NM, 1-Nov-2010.) (Proof shortened by Mario Carneiro, 19-Nov-2016.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (∃!𝑥∃𝑦 ∈ 𝐴 𝑥 = 𝐵 → (℩𝑥∃𝑦 ∈ 𝐴 𝑥 = 𝐵) = (℩𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵))
Theorem	f1ofveu 5527*	There is one domain element for each value of a one-to-one onto function. (Contributed by NM, 26-May-2006.)
⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → ∃!𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐶)
Theorem	f1ocnvfv3 5528*	Value of the converse of a one-to-one onto function. (Contributed by NM, 26-May-2006.) (Proof shortened by Mario Carneiro, 24-Dec-2016.)
⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → (◡𝐹‘𝐶) = (℩𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐶))
Theorem	riotaund 5529*	Restricted iota equals the empty set when not meaningful. (Contributed by NM, 16-Jan-2012.) (Revised by Mario Carneiro, 15-Oct-2016.) (Revised by NM, 13-Sep-2018.)
⊢ (¬ ∃!𝑥 ∈ 𝐴 𝜑 → (℩𝑥 ∈ 𝐴 𝜑) = ∅)
Theorem	acexmidlema 5530*	Lemma for acexmid 5538. (Contributed by Jim Kingdon, 6-Aug-2019.)
⊢ 𝐴 = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = ∅ ∨ 𝜑)}    &   ⊢ 𝐵 = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = {∅} ∨ 𝜑)}    &   ⊢ 𝐶 = {𝐴, 𝐵}    ⇒   ⊢ ({∅} ∈ 𝐴 → 𝜑)
Theorem	acexmidlemb 5531*	Lemma for acexmid 5538. (Contributed by Jim Kingdon, 6-Aug-2019.)
⊢ 𝐴 = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = ∅ ∨ 𝜑)}    &   ⊢ 𝐵 = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = {∅} ∨ 𝜑)}    &   ⊢ 𝐶 = {𝐴, 𝐵}    ⇒   ⊢ (∅ ∈ 𝐵 → 𝜑)
Theorem	acexmidlemph 5532*	Lemma for acexmid 5538. (Contributed by Jim Kingdon, 6-Aug-2019.)
⊢ 𝐴 = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = ∅ ∨ 𝜑)}    &   ⊢ 𝐵 = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = {∅} ∨ 𝜑)}    &   ⊢ 𝐶 = {𝐴, 𝐵}    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	acexmidlemab 5533*	Lemma for acexmid 5538. (Contributed by Jim Kingdon, 6-Aug-2019.)
⊢ 𝐴 = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = ∅ ∨ 𝜑)}    &   ⊢ 𝐵 = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = {∅} ∨ 𝜑)}    &   ⊢ 𝐶 = {𝐴, 𝐵}    ⇒   ⊢ (((℩𝑣 ∈ 𝐴 ∃𝑢 ∈ 𝑦 (𝐴 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢)) = ∅ ∧ (℩𝑣 ∈ 𝐵 ∃𝑢 ∈ 𝑦 (𝐵 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢)) = {∅}) → ¬ 𝜑)
Theorem	acexmidlemcase 5534*	Lemma for acexmid 5538. Here we divide the proof into cases (based on the disjunction implicit in an unordered pair, not the sort of case elimination which relies on excluded middle). The cases are (1) the choice function evaluated at 𝐴 equals {∅}, (2) the choice function evaluated at 𝐵 equals ∅, and (3) the choice function evaluated at 𝐴 equals ∅ and the choice function evaluated at 𝐵 equals {∅}. Because of the way we represent the choice function 𝑦, the choice function evaluated at 𝐴 is (℩𝑣 ∈ 𝐴∃𝑢 ∈ 𝑦(𝐴 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢)) and the choice function evaluated at 𝐵 is (℩𝑣 ∈ 𝐵∃𝑢 ∈ 𝑦(𝐵 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢)). Other than the difference in notation these work just as (𝑦‘𝐴) and (𝑦‘𝐵) would if 𝑦 were a function as defined by df-fun 4931. Although it isn't exactly about the division into cases, it is also convenient for this lemma to also include the step that if the choice function evaluated at 𝐴 equals {∅}, then {∅} ∈ 𝐴 and likewise for 𝐵. (Contributed by Jim Kingdon, 7-Aug-2019.)
⊢ 𝐴 = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = ∅ ∨ 𝜑)}    &   ⊢ 𝐵 = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = {∅} ∨ 𝜑)}    &   ⊢ 𝐶 = {𝐴, 𝐵}    ⇒   ⊢ (∀𝑧 ∈ 𝐶 ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) → ({∅} ∈ 𝐴 ∨ ∅ ∈ 𝐵 ∨ ((℩𝑣 ∈ 𝐴 ∃𝑢 ∈ 𝑦 (𝐴 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢)) = ∅ ∧ (℩𝑣 ∈ 𝐵 ∃𝑢 ∈ 𝑦 (𝐵 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢)) = {∅})))
Theorem	acexmidlem1 5535*	Lemma for acexmid 5538. List the cases identified in acexmidlemcase 5534 and hook them up to the lemmas which handle each case. (Contributed by Jim Kingdon, 7-Aug-2019.)
⊢ 𝐴 = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = ∅ ∨ 𝜑)}    &   ⊢ 𝐵 = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = {∅} ∨ 𝜑)}    &   ⊢ 𝐶 = {𝐴, 𝐵}    ⇒   ⊢ (∀𝑧 ∈ 𝐶 ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) → (𝜑 ∨ ¬ 𝜑))
Theorem	acexmidlem2 5536*	Lemma for acexmid 5538. This builds on acexmidlem1 5535 by noting that every element of 𝐶 is inhabited. (Note that 𝑦 is not quite a function in the df-fun 4931 sense because it uses ordered pairs as described in opthreg 4307 rather than df-op 3411). The set 𝐴 is also found in onsucelsucexmidlem 4281. (Contributed by Jim Kingdon, 5-Aug-2019.)
⊢ 𝐴 = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = ∅ ∨ 𝜑)}    &   ⊢ 𝐵 = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = {∅} ∨ 𝜑)}    &   ⊢ 𝐶 = {𝐴, 𝐵}    ⇒   ⊢ (∀𝑧 ∈ 𝐶 ∀𝑤 ∈ 𝑧 ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) → (𝜑 ∨ ¬ 𝜑))
Theorem	acexmidlemv 5537*	Lemma for acexmid 5538. This is acexmid 5538 with additional distinct variable constraints, most notably between 𝜑 and 𝑥. (Contributed by Jim Kingdon, 6-Aug-2019.)
⊢ ∃𝑦∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑧 ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢)    ⇒   ⊢ (𝜑 ∨ ¬ 𝜑)
Theorem	acexmid 5538*	The axiom of choice implies excluded middle. Theorem 1.3 in [Bauer] p. 483. The statement of the axiom of choice given here is ac2 in the Metamath Proof Explorer (version of 3-Aug-2019). In particular, note that the choice function 𝑦 provides a value when 𝑧 is inhabited (as opposed to non-empty as in some statements of the axiom of choice). Essentially the same proof can also be found at "The axiom of choice implies instances of EM", [Crosilla], p. "Set-theoretic principles incompatible with intuitionistic logic". Often referred to as Diaconescu's theorem, or Diaconescu-Goodman-Myhill theorem, after Radu Diaconescu who discovered it in 1975 in the framework of topos theory and N. D. Goodman and John Myhill in 1978 in the framework of set theory (although it already appeared as an exercise in Errett Bishop's book Foundations of Constructive Analysis from 1967). (Contributed by Jim Kingdon, 4-Aug-2019.)
⊢ ∃𝑦∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑧 ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢)    ⇒   ⊢ (𝜑 ∨ ¬ 𝜑)
2.6.10  Operations
Syntax	co 5539	Extend class notation to include the value of an operation 𝐹 (such as + ) for two arguments 𝐴 and 𝐵. Note that the syntax is simply three class symbols in a row surrounded by parentheses. Since operation values are the only possible class expressions consisting of three class expressions in a row surrounded by parentheses, the syntax is unambiguous.
class (𝐴𝐹𝐵)
Syntax	coprab 5540	Extend class notation to include class abstraction (class builder) of nested ordered pairs.
class {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}
Syntax	cmpt2 5541	Extend the definition of a class to include maps-to notation for defining an operation via a rule.
class (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
Definition	df-ov 5542	Define the value of an operation. Definition of operation value in [Enderton] p. 79. Note that the syntax is simply three class expressions in a row bracketed by parentheses. There are no restrictions of any kind on what those class expressions may be, although only certain kinds of class expressions - a binary operation 𝐹 and its arguments 𝐴 and 𝐵- will be useful for proving meaningful theorems. For example, if class 𝐹 is the operation + and arguments 𝐴 and 𝐵 are 3 and 2 , the expression ( 3 + 2 ) can be proved to equal 5 . This definition is well-defined, although not very meaningful, when classes 𝐴 and/or 𝐵 are proper classes (i.e. are not sets); see ovprc1 5568 and ovprc2 5569. On the other hand, we often find uses for this definition when 𝐹 is a proper class. 𝐹 is normally equal to a class of nested ordered pairs of the form defined by df-oprab 5543. (Contributed by NM, 28-Feb-1995.)
⊢ (𝐴𝐹𝐵) = (𝐹‘⟨𝐴, 𝐵⟩)
Definition	df-oprab 5543*	Define the class abstraction (class builder) of a collection of nested ordered pairs (for use in defining operations). This is a special case of Definition 4.16 of [TakeutiZaring] p. 14. Normally 𝑥, 𝑦, and 𝑧 are distinct, although the definition doesn't strictly require it. See df-ov 5542 for the value of an operation. The brace notation is called "class abstraction" by Quine; it is also called a "class builder" in the literature. The value of the most common operation class builder is given by ovmpt2 5663. (Contributed by NM, 12-Mar-1995.)
⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {𝑤 ∣ ∃𝑥∃𝑦∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)}
Definition	df-mpt2 5544*	Define maps-to notation for defining an operation via a rule. Read as "the operation defined by the map from 𝑥, 𝑦 (in 𝐴 × 𝐵) to 𝐵(𝑥, 𝑦)." An extension of df-mpt 3847 for two arguments. (Contributed by NM, 17-Feb-2008.)
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
Theorem	oveq 5545	Equality theorem for operation value. (Contributed by NM, 28-Feb-1995.)
⊢ (𝐹 = 𝐺 → (𝐴𝐹𝐵) = (𝐴𝐺𝐵))
Theorem	oveq1 5546	Equality theorem for operation value. (Contributed by NM, 28-Feb-1995.)
⊢ (𝐴 = 𝐵 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶))
Theorem	oveq2 5547	Equality theorem for operation value. (Contributed by NM, 28-Feb-1995.)
⊢ (𝐴 = 𝐵 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))
Theorem	oveq12 5548	Equality theorem for operation value. (Contributed by NM, 16-Jul-1995.)
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))
Theorem	oveq1i 5549	Equality inference for operation value. (Contributed by NM, 28-Feb-1995.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐴𝐹𝐶) = (𝐵𝐹𝐶)
Theorem	oveq2i 5550	Equality inference for operation value. (Contributed by NM, 28-Feb-1995.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐶𝐹𝐴) = (𝐶𝐹𝐵)
Theorem	oveq12i 5551	Equality inference for operation value. (Contributed by NM, 28-Feb-1995.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ (𝐴𝐹𝐶) = (𝐵𝐹𝐷)
Theorem	oveqi 5552	Equality inference for operation value. (Contributed by NM, 24-Nov-2007.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐶𝐴𝐷) = (𝐶𝐵𝐷)
Theorem	oveq123i 5553	Equality inference for operation value. (Contributed by FL, 11-Jul-2010.)
⊢ 𝐴 = 𝐶    &   ⊢ 𝐵 = 𝐷    &   ⊢ 𝐹 = 𝐺    ⇒   ⊢ (𝐴𝐹𝐵) = (𝐶𝐺𝐷)
Theorem	oveq1d 5554	Equality deduction for operation value. (Contributed by NM, 13-Mar-1995.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶))
Theorem	oveq2d 5555	Equality deduction for operation value. (Contributed by NM, 13-Mar-1995.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))
Theorem	oveqd 5556	Equality deduction for operation value. (Contributed by NM, 9-Sep-2006.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐶𝐴𝐷) = (𝐶𝐵𝐷))
Theorem	oveq12d 5557	Equality deduction for operation value. (Contributed by NM, 13-Mar-1995.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))
Theorem	oveqan12d 5558	Equality deduction for operation value. (Contributed by NM, 10-Aug-1995.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜓 → 𝐶 = 𝐷)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))
Theorem	oveqan12rd 5559	Equality deduction for operation value. (Contributed by NM, 10-Aug-1995.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜓 → 𝐶 = 𝐷)    ⇒   ⊢ ((𝜓 ∧ 𝜑) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))
Theorem	oveq123d 5560	Equality deduction for operation value. (Contributed by FL, 22-Dec-2008.)
⊢ (𝜑 → 𝐹 = 𝐺)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐴𝐹𝐶) = (𝐵𝐺𝐷))
Theorem	nfovd 5561	Deduction version of bound-variable hypothesis builder nfov 5562. (Contributed by NM, 13-Dec-2005.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
⊢ (𝜑 → Ⅎ𝑥𝐴)    &   ⊢ (𝜑 → Ⅎ𝑥𝐹)    &   ⊢ (𝜑 → Ⅎ𝑥𝐵)    ⇒   ⊢ (𝜑 → Ⅎ𝑥(𝐴𝐹𝐵))
Theorem	nfov 5562	Bound-variable hypothesis builder for operation value. (Contributed by NM, 4-May-2004.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐹    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥(𝐴𝐹𝐵)
Theorem	oprabidlem 5563*	Slight elaboration of exdistrfor 1697. A lemma for oprabid 5564. (Contributed by Jim Kingdon, 15-Jan-2019.)
⊢ (∃𝑥∃𝑦(𝑥 = 𝑧 ∧ 𝜓) → ∃𝑥(𝑥 = 𝑧 ∧ ∃𝑦𝜓))
Theorem	oprabid 5564	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 1415 to eliminate that constraint. (Contributed by Mario Carneiro, 20-Mar-2013.)
⊢ (⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∈ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} ↔ 𝜑)
Theorem	fnovex 5565	The result of an operation is a set. (Contributed by Jim Kingdon, 15-Jan-2019.)
⊢ ((𝐹 Fn (𝐶 × 𝐷) ∧ 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴𝐹𝐵) ∈ V)
Theorem	ovexg 5566	Evaluating a set operation at two sets gives a set. (Contributed by Jim Kingdon, 19-Aug-2021.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 ∈ 𝑊 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐹𝐵) ∈ V)
Theorem	ovprc 5567	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 5568	The value of an operation when the first argument is a proper class. (Contributed by NM, 16-Jun-2004.)
⊢ Rel dom 𝐹    ⇒   ⊢ (¬ 𝐴 ∈ V → (𝐴𝐹𝐵) = ∅)
Theorem	ovprc2 5569	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 5570	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 5571*	Move class substitution in and out of an operation. (Contributed by NM, 12-Nov-2005.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(𝐵𝐹𝐶) = (⦋𝐴 / 𝑥⦌𝐵𝐹⦋𝐴 / 𝑥⦌𝐶))
Theorem	csbov1g 5572*	Move class substitution in and out of an operation. (Contributed by NM, 12-Nov-2005.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(𝐵𝐹𝐶) = (⦋𝐴 / 𝑥⦌𝐵𝐹𝐶))
Theorem	csbov2g 5573*	Move class substitution in and out of an operation. (Contributed by NM, 12-Nov-2005.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(𝐵𝐹𝐶) = (𝐵𝐹⦋𝐴 / 𝑥⦌𝐶))
Theorem	rspceov 5574*	A frequently used special case of rspc2ev 2686 for operation values. (Contributed by NM, 21-Mar-2007.)
⊢ ((𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ∧ 𝑆 = (𝐶𝐹𝐷)) → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑆 = (𝑥𝐹𝑦))
Theorem	fnotovb 5575	Equivalence of operation value and ordered triple membership, analogous to fnopfvb 5242. (Contributed by NM, 17-Dec-2008.) (Revised by Mario Carneiro, 28-Apr-2015.)
⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵) → ((𝐶𝐹𝐷) = 𝑅 ↔ ⟨𝐶, 𝐷, 𝑅⟩ ∈ 𝐹))
Theorem	opabbrex 5576*	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 5577	The empty set is never an element in an ordered-pair class abstraction. (Contributed by Alexander van der Vekens, 5-Nov-2017.)
⊢ ¬ ∅ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑}
Theorem	brabvv 5578*	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 5579*	Class abstraction for operations in terms of class abstraction of ordered pairs. (Contributed by NM, 12-Mar-1995.)
⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {⟨𝑤, 𝑧⟩ ∣ ∃𝑥∃𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
Theorem	reloprab 5580*	An operation class abstraction is a relation. (Contributed by NM, 16-Jun-2004.)
⊢ Rel {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}
Theorem	nfoprab1 5581	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 5582	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 5583	The abstraction variables in an operation class abstraction are not free. (Contributed by NM, 22-Aug-2013.)
⊢ Ⅎ𝑧{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}
Theorem	nfoprab 5584*	Bound-variable hypothesis builder for an operation class abstraction. (Contributed by NM, 22-Aug-2013.)
⊢ Ⅎ𝑤𝜑    ⇒   ⊢ Ⅎ𝑤{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}
Theorem	oprabbid 5585*	Equivalent wff's yield equal operation class abstractions (deduction rule). (Contributed by NM, 21-Feb-2004.) (Revised by Mario Carneiro, 24-Jun-2014.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑧𝜑    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜒})
Theorem	oprabbidv 5586*	Equivalent wff's yield equal operation class abstractions (deduction rule). (Contributed by NM, 21-Feb-2004.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜒})
Theorem	oprabbii 5587*	Equivalent wff's yield equal operation class abstractions. (Contributed by NM, 28-May-1995.) (Revised by David Abernethy, 19-Jun-2012.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓}
Theorem	ssoprab2 5588	Equivalence of ordered pair abstraction subclass and implication. Compare ssopab2 4039. (Contributed by FL, 6-Nov-2013.) (Proof shortened by Mario Carneiro, 11-Dec-2016.)
⊢ (∀𝑥∀𝑦∀𝑧(𝜑 → 𝜓) → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} ⊆ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓})
Theorem	ssoprab2b 5589	Equivalence of ordered pair abstraction subclass and implication. Compare ssopab2b 4040. (Contributed by FL, 6-Nov-2013.) (Proof shortened by Mario Carneiro, 11-Dec-2016.)
⊢ ({⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} ⊆ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} ↔ ∀𝑥∀𝑦∀𝑧(𝜑 → 𝜓))
Theorem	eqoprab2b 5590	Equivalence of ordered pair abstraction subclass and biconditional. Compare eqopab2b 4043. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ ({⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} ↔ ∀𝑥∀𝑦∀𝑧(𝜑 ↔ 𝜓))
Theorem	mpt2eq123 5591*	An equality theorem for the maps to notation. (Contributed by Mario Carneiro, 16-Dec-2013.) (Revised by Mario Carneiro, 19-Mar-2015.)
⊢ ((𝐴 = 𝐷 ∧ ∀𝑥 ∈ 𝐴 (𝐵 = 𝐸 ∧ ∀𝑦 ∈ 𝐵 𝐶 = 𝐹)) → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐷, 𝑦 ∈ 𝐸 ↦ 𝐹))
Theorem	mpt2eq12 5592*	An equality theorem for the maps to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐸) = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝐸))
Theorem	mpt2eq123dva 5593*	An equality deduction for the maps to notation. (Contributed by Mario Carneiro, 26-Jan-2017.)
⊢ (𝜑 → 𝐴 = 𝐷)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐸)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝐶 = 𝐹)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐷, 𝑦 ∈ 𝐸 ↦ 𝐹))
Theorem	mpt2eq123dv 5594*	An equality deduction for the maps to notation. (Contributed by NM, 12-Sep-2011.)
⊢ (𝜑 → 𝐴 = 𝐷)    &   ⊢ (𝜑 → 𝐵 = 𝐸)    &   ⊢ (𝜑 → 𝐶 = 𝐹)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐷, 𝑦 ∈ 𝐸 ↦ 𝐹))
Theorem	mpt2eq123i 5595	An equality inference for the maps to notation. (Contributed by NM, 15-Jul-2013.)
⊢ 𝐴 = 𝐷    &   ⊢ 𝐵 = 𝐸    &   ⊢ 𝐶 = 𝐹    ⇒   ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐷, 𝑦 ∈ 𝐸 ↦ 𝐹)
Theorem	mpt2eq3dva 5596*	Slightly more general equality inference for the maps to notation. (Contributed by NM, 17-Oct-2013.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷))
Theorem	mpt2eq3ia 5597	An equality inference for the maps to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐶 = 𝐷)    ⇒   ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷)
Theorem	nfmpt21 5598	Bound-variable hypothesis builder for an operation in maps-to notation. (Contributed by NM, 27-Aug-2013.)
⊢ Ⅎ𝑥(𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
Theorem	nfmpt22 5599	Bound-variable hypothesis builder for an operation in maps-to notation. (Contributed by NM, 27-Aug-2013.)
⊢ Ⅎ𝑦(𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
Theorem	nfmpt2 5600*	Bound-variable hypothesis builder for the maps-to notation. (Contributed by NM, 20-Feb-2013.)
⊢ Ⅎ𝑧𝐴    &   ⊢ Ⅎ𝑧𝐵    &   ⊢ Ⅎ𝑧𝐶    ⇒   ⊢ Ⅎ𝑧(𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)