HomeHome Intuitionistic Logic Explorer
Theorem List (p. 59 of 149)
< 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 - 5801-5900   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremfliftval 5801* The value of the function ๐น. (Contributed by Mario Carneiro, 23-Dec-2016.)
๐น = ran (๐‘ฅ โˆˆ ๐‘‹ โ†ฆ โŸจ๐ด, ๐ตโŸฉ)    &   ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹) โ†’ ๐ด โˆˆ ๐‘…)    &   ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹) โ†’ ๐ต โˆˆ ๐‘†)    &   (๐‘ฅ = ๐‘Œ โ†’ ๐ด = ๐ถ)    &   (๐‘ฅ = ๐‘Œ โ†’ ๐ต = ๐ท)    &   (๐œ‘ โ†’ Fun ๐น)    โ‡’   ((๐œ‘ โˆง ๐‘Œ โˆˆ ๐‘‹) โ†’ (๐นโ€˜๐ถ) = ๐ท)
 
Theoremisoeq1 5802 Equality theorem for isomorphisms. (Contributed by NM, 17-May-2004.)
(๐ป = ๐บ โ†’ (๐ป Isom ๐‘…, ๐‘† (๐ด, ๐ต) โ†” ๐บ Isom ๐‘…, ๐‘† (๐ด, ๐ต)))
 
Theoremisoeq2 5803 Equality theorem for isomorphisms. (Contributed by NM, 17-May-2004.)
(๐‘… = ๐‘‡ โ†’ (๐ป Isom ๐‘…, ๐‘† (๐ด, ๐ต) โ†” ๐ป Isom ๐‘‡, ๐‘† (๐ด, ๐ต)))
 
Theoremisoeq3 5804 Equality theorem for isomorphisms. (Contributed by NM, 17-May-2004.)
(๐‘† = ๐‘‡ โ†’ (๐ป Isom ๐‘…, ๐‘† (๐ด, ๐ต) โ†” ๐ป Isom ๐‘…, ๐‘‡ (๐ด, ๐ต)))
 
Theoremisoeq4 5805 Equality theorem for isomorphisms. (Contributed by NM, 17-May-2004.)
(๐ด = ๐ถ โ†’ (๐ป Isom ๐‘…, ๐‘† (๐ด, ๐ต) โ†” ๐ป Isom ๐‘…, ๐‘† (๐ถ, ๐ต)))
 
Theoremisoeq5 5806 Equality theorem for isomorphisms. (Contributed by NM, 17-May-2004.)
(๐ต = ๐ถ โ†’ (๐ป Isom ๐‘…, ๐‘† (๐ด, ๐ต) โ†” ๐ป Isom ๐‘…, ๐‘† (๐ด, ๐ถ)))
 
Theoremnfiso 5807 Bound-variable hypothesis builder for an isomorphism. (Contributed by NM, 17-May-2004.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
โ„ฒ๐‘ฅ๐ป    &   โ„ฒ๐‘ฅ๐‘…    &   โ„ฒ๐‘ฅ๐‘†    &   โ„ฒ๐‘ฅ๐ด    &   โ„ฒ๐‘ฅ๐ต    โ‡’   โ„ฒ๐‘ฅ ๐ป Isom ๐‘…, ๐‘† (๐ด, ๐ต)
 
Theoremisof1o 5808 An isomorphism is a one-to-one onto function. (Contributed by NM, 27-Apr-2004.)
(๐ป Isom ๐‘…, ๐‘† (๐ด, ๐ต) โ†’ ๐ป:๐ดโ€“1-1-ontoโ†’๐ต)
 
Theoremisorel 5809 An isomorphism connects binary relations via its function values. (Contributed by NM, 27-Apr-2004.)
((๐ป Isom ๐‘…, ๐‘† (๐ด, ๐ต) โˆง (๐ถ โˆˆ ๐ด โˆง ๐ท โˆˆ ๐ด)) โ†’ (๐ถ๐‘…๐ท โ†” (๐ปโ€˜๐ถ)๐‘†(๐ปโ€˜๐ท)))
 
Theoremisoresbr 5810* A consequence of isomorphism on two relations for a function's restriction. (Contributed by Jim Kingdon, 11-Jan-2019.)
((๐น โ†พ ๐ด) Isom ๐‘…, ๐‘† (๐ด, (๐น โ€œ ๐ด)) โ†’ โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ด (๐‘ฅ๐‘…๐‘ฆ โ†’ (๐นโ€˜๐‘ฅ)๐‘†(๐นโ€˜๐‘ฆ)))
 
Theoremisoid 5811 Identity law for isomorphism. Proposition 6.30(1) of [TakeutiZaring] p. 33. (Contributed by NM, 27-Apr-2004.)
( I โ†พ ๐ด) Isom ๐‘…, ๐‘… (๐ด, ๐ด)
 
Theoremisocnv 5812 Converse law for isomorphism. Proposition 6.30(2) of [TakeutiZaring] p. 33. (Contributed by NM, 27-Apr-2004.)
(๐ป Isom ๐‘…, ๐‘† (๐ด, ๐ต) โ†’ โ—ก๐ป Isom ๐‘†, ๐‘… (๐ต, ๐ด))
 
Theoremisocnv2 5813 Converse law for isomorphism. (Contributed by Mario Carneiro, 30-Jan-2014.)
(๐ป Isom ๐‘…, ๐‘† (๐ด, ๐ต) โ†” ๐ป Isom โ—ก๐‘…, โ—ก๐‘†(๐ด, ๐ต))
 
Theoremisores2 5814 An isomorphism from one well-order to another can be restricted on either well-order. (Contributed by Mario Carneiro, 15-Jan-2013.)
(๐ป Isom ๐‘…, ๐‘† (๐ด, ๐ต) โ†” ๐ป Isom ๐‘…, (๐‘† โˆฉ (๐ต ร— ๐ต))(๐ด, ๐ต))
 
Theoremisores1 5815 An isomorphism from one well-order to another can be restricted on either well-order. (Contributed by Mario Carneiro, 15-Jan-2013.)
(๐ป Isom ๐‘…, ๐‘† (๐ด, ๐ต) โ†” ๐ป Isom (๐‘… โˆฉ (๐ด ร— ๐ด)), ๐‘†(๐ด, ๐ต))
 
Theoremisores3 5816 Induced isomorphism on a subset. (Contributed by Stefan O'Rear, 5-Nov-2014.)
((๐ป Isom ๐‘…, ๐‘† (๐ด, ๐ต) โˆง ๐พ โŠ† ๐ด โˆง ๐‘‹ = (๐ป โ€œ ๐พ)) โ†’ (๐ป โ†พ ๐พ) Isom ๐‘…, ๐‘† (๐พ, ๐‘‹))
 
Theoremisotr 5817 Composition (transitive) law for isomorphism. Proposition 6.30(3) of [TakeutiZaring] p. 33. (Contributed by NM, 27-Apr-2004.) (Proof shortened by Mario Carneiro, 5-Dec-2016.)
((๐ป Isom ๐‘…, ๐‘† (๐ด, ๐ต) โˆง ๐บ Isom ๐‘†, ๐‘‡ (๐ต, ๐ถ)) โ†’ (๐บ โˆ˜ ๐ป) Isom ๐‘…, ๐‘‡ (๐ด, ๐ถ))
 
Theoremiso0 5818 The empty set is an ๐‘…, ๐‘† isomorphism from the empty set to the empty set. (Contributed by Steve Rodriguez, 24-Oct-2015.)
โˆ… Isom ๐‘…, ๐‘† (โˆ…, โˆ…)
 
Theoremisoini 5819 Isomorphisms preserve initial segments. Proposition 6.31(2) of [TakeutiZaring] p. 33. (Contributed by NM, 20-Apr-2004.)
((๐ป Isom ๐‘…, ๐‘† (๐ด, ๐ต) โˆง ๐ท โˆˆ ๐ด) โ†’ (๐ป โ€œ (๐ด โˆฉ (โ—ก๐‘… โ€œ {๐ท}))) = (๐ต โˆฉ (โ—ก๐‘† โ€œ {(๐ปโ€˜๐ท)})))
 
Theoremisoini2 5820 Isomorphisms are isomorphisms on their initial segments. (Contributed by Mario Carneiro, 29-Mar-2014.)
๐ถ = (๐ด โˆฉ (โ—ก๐‘… โ€œ {๐‘‹}))    &   ๐ท = (๐ต โˆฉ (โ—ก๐‘† โ€œ {(๐ปโ€˜๐‘‹)}))    โ‡’   ((๐ป Isom ๐‘…, ๐‘† (๐ด, ๐ต) โˆง ๐‘‹ โˆˆ ๐ด) โ†’ (๐ป โ†พ ๐ถ) Isom ๐‘…, ๐‘† (๐ถ, ๐ท))
 
Theoremisoselem 5821* Lemma for isose 5822. (Contributed by Mario Carneiro, 23-Jun-2015.)
(๐œ‘ โ†’ ๐ป Isom ๐‘…, ๐‘† (๐ด, ๐ต))    &   (๐œ‘ โ†’ (๐ป โ€œ ๐‘ฅ) โˆˆ V)    โ‡’   (๐œ‘ โ†’ (๐‘… Se ๐ด โ†’ ๐‘† Se ๐ต))
 
Theoremisose 5822 An isomorphism preserves set-like relations. (Contributed by Mario Carneiro, 23-Jun-2015.)
(๐ป Isom ๐‘…, ๐‘† (๐ด, ๐ต) โ†’ (๐‘… Se ๐ด โ†” ๐‘† Se ๐ต))
 
Theoremisopolem 5823 Lemma for isopo 5824. (Contributed by Stefan O'Rear, 16-Nov-2014.)
(๐ป Isom ๐‘…, ๐‘† (๐ด, ๐ต) โ†’ (๐‘† Po ๐ต โ†’ ๐‘… Po ๐ด))
 
Theoremisopo 5824 An isomorphism preserves partial ordering. (Contributed by Stefan O'Rear, 16-Nov-2014.)
(๐ป Isom ๐‘…, ๐‘† (๐ด, ๐ต) โ†’ (๐‘… Po ๐ด โ†” ๐‘† Po ๐ต))
 
Theoremisosolem 5825 Lemma for isoso 5826. (Contributed by Stefan O'Rear, 16-Nov-2014.)
(๐ป Isom ๐‘…, ๐‘† (๐ด, ๐ต) โ†’ (๐‘† Or ๐ต โ†’ ๐‘… Or ๐ด))
 
Theoremisoso 5826 An isomorphism preserves strict ordering. (Contributed by Stefan O'Rear, 16-Nov-2014.)
(๐ป Isom ๐‘…, ๐‘† (๐ด, ๐ต) โ†’ (๐‘… Or ๐ด โ†” ๐‘† Or ๐ต))
 
Theoremf1oiso 5827* Any one-to-one onto function determines an isomorphism with an induced relation ๐‘†. Proposition 6.33 of [TakeutiZaring] p. 34. (Contributed by NM, 30-Apr-2004.)
((๐ป:๐ดโ€“1-1-ontoโ†’๐ต โˆง ๐‘† = {โŸจ๐‘ง, ๐‘คโŸฉ โˆฃ โˆƒ๐‘ฅ โˆˆ ๐ด โˆƒ๐‘ฆ โˆˆ ๐ด ((๐‘ง = (๐ปโ€˜๐‘ฅ) โˆง ๐‘ค = (๐ปโ€˜๐‘ฆ)) โˆง ๐‘ฅ๐‘…๐‘ฆ)}) โ†’ ๐ป Isom ๐‘…, ๐‘† (๐ด, ๐ต))
 
Theoremf1oiso2 5828* Any one-to-one onto function determines an isomorphism with an induced relation ๐‘†. (Contributed by Mario Carneiro, 9-Mar-2013.)
๐‘† = {โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆฃ ((๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ต) โˆง (โ—ก๐ปโ€˜๐‘ฅ)๐‘…(โ—ก๐ปโ€˜๐‘ฆ))}    โ‡’   (๐ป:๐ดโ€“1-1-ontoโ†’๐ต โ†’ ๐ป Isom ๐‘…, ๐‘† (๐ด, ๐ต))
 
2.6.9  Cantor's Theorem
 
Theoremcanth 5829 No set ๐ด is equinumerous to its power set (Cantor's theorem), i.e., no function can map ๐ด onto its power set. Compare Theorem 6B(b) of [Enderton] p. 132. (Use nex 1500 if you want the form ยฌ โˆƒ๐‘“๐‘“:๐ดโ€“ontoโ†’๐’ซ ๐ด.) (Contributed by NM, 7-Aug-1994.) (Revised by Noah R Kingdon, 23-Jul-2024.)
๐ด โˆˆ V    โ‡’    ยฌ ๐น:๐ดโ€“ontoโ†’๐’ซ ๐ด
 
2.6.10  Restricted iota (description binder)
 
Syntaxcrio 5830 Extend class notation with restricted description binder.
class (โ„ฉ๐‘ฅ โˆˆ ๐ด ๐œ‘)
 
Definitiondf-riota 5831 Define restricted description binder. In case there is no unique ๐‘ฅ such that (๐‘ฅ โˆˆ ๐ด โˆง ๐œ‘) holds, it evaluates to the empty set. See also comments for df-iota 5179. (Contributed by NM, 15-Sep-2011.) (Revised by Mario Carneiro, 15-Oct-2016.) (Revised by NM, 2-Sep-2018.)
(โ„ฉ๐‘ฅ โˆˆ ๐ด ๐œ‘) = (โ„ฉ๐‘ฅ(๐‘ฅ โˆˆ ๐ด โˆง ๐œ‘))
 
Theoremriotaeqdv 5832* Formula-building deduction for iota. (Contributed by NM, 15-Sep-2011.)
(๐œ‘ โ†’ ๐ด = ๐ต)    โ‡’   (๐œ‘ โ†’ (โ„ฉ๐‘ฅ โˆˆ ๐ด ๐œ“) = (โ„ฉ๐‘ฅ โˆˆ ๐ต ๐œ“))
 
Theoremriotabidv 5833* Formula-building deduction for restricted iota. (Contributed by NM, 15-Sep-2011.)
(๐œ‘ โ†’ (๐œ“ โ†” ๐œ’))    โ‡’   (๐œ‘ โ†’ (โ„ฉ๐‘ฅ โˆˆ ๐ด ๐œ“) = (โ„ฉ๐‘ฅ โˆˆ ๐ด ๐œ’))
 
Theoremriotaeqbidv 5834* Equality deduction for restricted universal quantifier. (Contributed by NM, 15-Sep-2011.)
(๐œ‘ โ†’ ๐ด = ๐ต)    &   (๐œ‘ โ†’ (๐œ“ โ†” ๐œ’))    โ‡’   (๐œ‘ โ†’ (โ„ฉ๐‘ฅ โˆˆ ๐ด ๐œ“) = (โ„ฉ๐‘ฅ โˆˆ ๐ต ๐œ’))
 
Theoremriotaexg 5835* Restricted iota is a set. (Contributed by Jim Kingdon, 15-Jun-2020.)
(๐ด โˆˆ ๐‘‰ โ†’ (โ„ฉ๐‘ฅ โˆˆ ๐ด ๐œ“) โˆˆ V)
 
Theoremriotav 5836 An iota restricted to the universe is unrestricted. (Contributed by NM, 18-Sep-2011.)
(โ„ฉ๐‘ฅ โˆˆ V ๐œ‘) = (โ„ฉ๐‘ฅ๐œ‘)
 
Theoremriotauni 5837 Restricted iota in terms of class union. (Contributed by NM, 11-Oct-2011.)
(โˆƒ!๐‘ฅ โˆˆ ๐ด ๐œ‘ โ†’ (โ„ฉ๐‘ฅ โˆˆ ๐ด ๐œ‘) = โˆช {๐‘ฅ โˆˆ ๐ด โˆฃ ๐œ‘})
 
Theoremnfriota1 5838* The abstraction variable in a restricted iota descriptor isn't free. (Contributed by NM, 12-Oct-2011.) (Revised by Mario Carneiro, 15-Oct-2016.)
โ„ฒ๐‘ฅ(โ„ฉ๐‘ฅ โˆˆ ๐ด ๐œ‘)
 
Theoremnfriotadxy 5839* Deduction version of nfriota 5840. (Contributed by Jim Kingdon, 12-Jan-2019.)
โ„ฒ๐‘ฆ๐œ‘    &   (๐œ‘ โ†’ โ„ฒ๐‘ฅ๐œ“)    &   (๐œ‘ โ†’ โ„ฒ๐‘ฅ๐ด)    โ‡’   (๐œ‘ โ†’ โ„ฒ๐‘ฅ(โ„ฉ๐‘ฆ โˆˆ ๐ด ๐œ“))
 
Theoremnfriota 5840* A variable not free in a wff remains so in a restricted iota descriptor. (Contributed by NM, 12-Oct-2011.)
โ„ฒ๐‘ฅ๐œ‘    &   โ„ฒ๐‘ฅ๐ด    โ‡’   โ„ฒ๐‘ฅ(โ„ฉ๐‘ฆ โˆˆ ๐ด ๐œ‘)
 
Theoremcbvriota 5841* Change bound variable in a restricted description binder. (Contributed by NM, 18-Mar-2013.) (Revised by Mario Carneiro, 15-Oct-2016.)
โ„ฒ๐‘ฆ๐œ‘    &   โ„ฒ๐‘ฅ๐œ“    &   (๐‘ฅ = ๐‘ฆ โ†’ (๐œ‘ โ†” ๐œ“))    โ‡’   (โ„ฉ๐‘ฅ โˆˆ ๐ด ๐œ‘) = (โ„ฉ๐‘ฆ โˆˆ ๐ด ๐œ“)
 
Theoremcbvriotav 5842* Change bound variable in a restricted description binder. (Contributed by NM, 18-Mar-2013.) (Revised by Mario Carneiro, 15-Oct-2016.)
(๐‘ฅ = ๐‘ฆ โ†’ (๐œ‘ โ†” ๐œ“))    โ‡’   (โ„ฉ๐‘ฅ โˆˆ ๐ด ๐œ‘) = (โ„ฉ๐‘ฆ โˆˆ ๐ด ๐œ“)
 
Theoremcsbriotag 5843* Interchange class substitution and restricted description binder. (Contributed by NM, 24-Feb-2013.)
(๐ด โˆˆ ๐‘‰ โ†’ โฆ‹๐ด / ๐‘ฅโฆŒ(โ„ฉ๐‘ฆ โˆˆ ๐ต ๐œ‘) = (โ„ฉ๐‘ฆ โˆˆ ๐ต [๐ด / ๐‘ฅ]๐œ‘))
 
Theoremriotacl2 5844 Membership law for "the unique element in ๐ด such that ๐œ‘."

(Contributed by NM, 21-Aug-2011.) (Revised by Mario Carneiro, 23-Dec-2016.)

(โˆƒ!๐‘ฅ โˆˆ ๐ด ๐œ‘ โ†’ (โ„ฉ๐‘ฅ โˆˆ ๐ด ๐œ‘) โˆˆ {๐‘ฅ โˆˆ ๐ด โˆฃ ๐œ‘})
 
Theoremriotacl 5845* Closure of restricted iota. (Contributed by NM, 21-Aug-2011.)
(โˆƒ!๐‘ฅ โˆˆ ๐ด ๐œ‘ โ†’ (โ„ฉ๐‘ฅ โˆˆ ๐ด ๐œ‘) โˆˆ ๐ด)
 
Theoremriotasbc 5846 Substitution law for descriptions. (Contributed by NM, 23-Aug-2011.) (Proof shortened by Mario Carneiro, 24-Dec-2016.)
(โˆƒ!๐‘ฅ โˆˆ ๐ด ๐œ‘ โ†’ [(โ„ฉ๐‘ฅ โˆˆ ๐ด ๐œ‘) / ๐‘ฅ]๐œ‘)
 
Theoremriotabidva 5847* Equivalent wff's yield equal restricted class abstractions (deduction form). (rabbidva 2726 analog.) (Contributed by NM, 17-Jan-2012.)
((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ด) โ†’ (๐œ“ โ†” ๐œ’))    โ‡’   (๐œ‘ โ†’ (โ„ฉ๐‘ฅ โˆˆ ๐ด ๐œ“) = (โ„ฉ๐‘ฅ โˆˆ ๐ด ๐œ’))
 
Theoremriotabiia 5848 Equivalent wff's yield equal restricted iotas (inference form). (rabbiia 2723 analog.) (Contributed by NM, 16-Jan-2012.)
(๐‘ฅ โˆˆ ๐ด โ†’ (๐œ‘ โ†” ๐œ“))    โ‡’   (โ„ฉ๐‘ฅ โˆˆ ๐ด ๐œ‘) = (โ„ฉ๐‘ฅ โˆˆ ๐ด ๐œ“)
 
Theoremriota1 5849* Property of restricted iota. Compare iota1 5193. (Contributed by Mario Carneiro, 15-Oct-2016.)
(โˆƒ!๐‘ฅ โˆˆ ๐ด ๐œ‘ โ†’ ((๐‘ฅ โˆˆ ๐ด โˆง ๐œ‘) โ†” (โ„ฉ๐‘ฅ โˆˆ ๐ด ๐œ‘) = ๐‘ฅ))
 
Theoremriota1a 5850 Property of iota. (Contributed by NM, 23-Aug-2011.)
((๐‘ฅ โˆˆ ๐ด โˆง โˆƒ!๐‘ฅ โˆˆ ๐ด ๐œ‘) โ†’ (๐œ‘ โ†” (โ„ฉ๐‘ฅ(๐‘ฅ โˆˆ ๐ด โˆง ๐œ‘)) = ๐‘ฅ))
 
Theoremriota2df 5851* A deduction version of riota2f 5852. (Contributed by NM, 17-Feb-2013.) (Revised by Mario Carneiro, 15-Oct-2016.)
โ„ฒ๐‘ฅ๐œ‘    &   (๐œ‘ โ†’ โ„ฒ๐‘ฅ๐ต)    &   (๐œ‘ โ†’ โ„ฒ๐‘ฅ๐œ’)    &   (๐œ‘ โ†’ ๐ต โˆˆ ๐ด)    &   ((๐œ‘ โˆง ๐‘ฅ = ๐ต) โ†’ (๐œ“ โ†” ๐œ’))    โ‡’   ((๐œ‘ โˆง โˆƒ!๐‘ฅ โˆˆ ๐ด ๐œ“) โ†’ (๐œ’ โ†” (โ„ฉ๐‘ฅ โˆˆ ๐ด ๐œ“) = ๐ต))
 
Theoremriota2f 5852* 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.)
โ„ฒ๐‘ฅ๐ต    &   โ„ฒ๐‘ฅ๐œ“    &   (๐‘ฅ = ๐ต โ†’ (๐œ‘ โ†” ๐œ“))    โ‡’   ((๐ต โˆˆ ๐ด โˆง โˆƒ!๐‘ฅ โˆˆ ๐ด ๐œ‘) โ†’ (๐œ“ โ†” (โ„ฉ๐‘ฅ โˆˆ ๐ด ๐œ‘) = ๐ต))
 
Theoremriota2 5853* 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.)
(๐‘ฅ = ๐ต โ†’ (๐œ‘ โ†” ๐œ“))    โ‡’   ((๐ต โˆˆ ๐ด โˆง โˆƒ!๐‘ฅ โˆˆ ๐ด ๐œ‘) โ†’ (๐œ“ โ†” (โ„ฉ๐‘ฅ โˆˆ ๐ด ๐œ‘) = ๐ต))
 
Theoremriotaprop 5854* Properties of a restricted definite description operator. Todo (df-riota 5831 update): can some uses of riota2f 5852 be shortened with this? (Contributed by NM, 23-Nov-2013.)
โ„ฒ๐‘ฅ๐œ“    &   ๐ต = (โ„ฉ๐‘ฅ โˆˆ ๐ด ๐œ‘)    &   (๐‘ฅ = ๐ต โ†’ (๐œ‘ โ†” ๐œ“))    โ‡’   (โˆƒ!๐‘ฅ โˆˆ ๐ด ๐œ‘ โ†’ (๐ต โˆˆ ๐ด โˆง ๐œ“))
 
Theoremriota5f 5855* A method for computing restricted iota. (Contributed by NM, 16-Apr-2013.) (Revised by Mario Carneiro, 15-Oct-2016.)
(๐œ‘ โ†’ โ„ฒ๐‘ฅ๐ต)    &   (๐œ‘ โ†’ ๐ต โˆˆ ๐ด)    &   ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ด) โ†’ (๐œ“ โ†” ๐‘ฅ = ๐ต))    โ‡’   (๐œ‘ โ†’ (โ„ฉ๐‘ฅ โˆˆ ๐ด ๐œ“) = ๐ต)
 
Theoremriota5 5856* A method for computing restricted iota. (Contributed by NM, 20-Oct-2011.) (Revised by Mario Carneiro, 6-Dec-2016.)
(๐œ‘ โ†’ ๐ต โˆˆ ๐ด)    &   ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ด) โ†’ (๐œ“ โ†” ๐‘ฅ = ๐ต))    โ‡’   (๐œ‘ โ†’ (โ„ฉ๐‘ฅ โˆˆ ๐ด ๐œ“) = ๐ต)
 
Theoremriotass2 5857* Restriction of a unique element to a smaller class. (Contributed by NM, 21-Aug-2011.) (Revised by NM, 22-Mar-2013.)
(((๐ด โŠ† ๐ต โˆง โˆ€๐‘ฅ โˆˆ ๐ด (๐œ‘ โ†’ ๐œ“)) โˆง (โˆƒ๐‘ฅ โˆˆ ๐ด ๐œ‘ โˆง โˆƒ!๐‘ฅ โˆˆ ๐ต ๐œ“)) โ†’ (โ„ฉ๐‘ฅ โˆˆ ๐ด ๐œ‘) = (โ„ฉ๐‘ฅ โˆˆ ๐ต ๐œ“))
 
Theoremriotass 5858* Restriction of a unique element to a smaller class. (Contributed by NM, 19-Oct-2005.) (Revised by Mario Carneiro, 24-Dec-2016.)
((๐ด โŠ† ๐ต โˆง โˆƒ๐‘ฅ โˆˆ ๐ด ๐œ‘ โˆง โˆƒ!๐‘ฅ โˆˆ ๐ต ๐œ‘) โ†’ (โ„ฉ๐‘ฅ โˆˆ ๐ด ๐œ‘) = (โ„ฉ๐‘ฅ โˆˆ ๐ต ๐œ‘))
 
Theoremmoriotass 5859* Restriction of a unique element to a smaller class. (Contributed by NM, 19-Feb-2006.) (Revised by NM, 16-Jun-2017.)
((๐ด โŠ† ๐ต โˆง โˆƒ๐‘ฅ โˆˆ ๐ด ๐œ‘ โˆง โˆƒ*๐‘ฅ โˆˆ ๐ต ๐œ‘) โ†’ (โ„ฉ๐‘ฅ โˆˆ ๐ด ๐œ‘) = (โ„ฉ๐‘ฅ โˆˆ ๐ต ๐œ‘))
 
Theoremsnriota 5860 A restricted class abstraction with a unique member can be expressed as a singleton. (Contributed by NM, 30-May-2006.)
(โˆƒ!๐‘ฅ โˆˆ ๐ด ๐œ‘ โ†’ {๐‘ฅ โˆˆ ๐ด โˆฃ ๐œ‘} = {(โ„ฉ๐‘ฅ โˆˆ ๐ด ๐œ‘)})
 
Theoremeusvobj2 5861* 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    โ‡’   (โˆƒ!๐‘ฅโˆƒ๐‘ฆ โˆˆ ๐ด ๐‘ฅ = ๐ต โ†’ (โˆƒ๐‘ฆ โˆˆ ๐ด ๐‘ฅ = ๐ต โ†” โˆ€๐‘ฆ โˆˆ ๐ด ๐‘ฅ = ๐ต))
 
Theoremeusvobj1 5862* 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    โ‡’   (โˆƒ!๐‘ฅโˆƒ๐‘ฆ โˆˆ ๐ด ๐‘ฅ = ๐ต โ†’ (โ„ฉ๐‘ฅโˆƒ๐‘ฆ โˆˆ ๐ด ๐‘ฅ = ๐ต) = (โ„ฉ๐‘ฅโˆ€๐‘ฆ โˆˆ ๐ด ๐‘ฅ = ๐ต))
 
Theoremf1ofveu 5863* There is one domain element for each value of a one-to-one onto function. (Contributed by NM, 26-May-2006.)
((๐น:๐ดโ€“1-1-ontoโ†’๐ต โˆง ๐ถ โˆˆ ๐ต) โ†’ โˆƒ!๐‘ฅ โˆˆ ๐ด (๐นโ€˜๐‘ฅ) = ๐ถ)
 
Theoremf1ocnvfv3 5864* 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โ†’๐ต โˆง ๐ถ โˆˆ ๐ต) โ†’ (โ—ก๐นโ€˜๐ถ) = (โ„ฉ๐‘ฅ โˆˆ ๐ด (๐นโ€˜๐‘ฅ) = ๐ถ))
 
Theoremriotaund 5865* 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.)
(ยฌ โˆƒ!๐‘ฅ โˆˆ ๐ด ๐œ‘ โ†’ (โ„ฉ๐‘ฅ โˆˆ ๐ด ๐œ‘) = โˆ…)
 
Theoremacexmidlema 5866* Lemma for acexmid 5874. (Contributed by Jim Kingdon, 6-Aug-2019.)
๐ด = {๐‘ฅ โˆˆ {โˆ…, {โˆ…}} โˆฃ (๐‘ฅ = โˆ… โˆจ ๐œ‘)}    &   ๐ต = {๐‘ฅ โˆˆ {โˆ…, {โˆ…}} โˆฃ (๐‘ฅ = {โˆ…} โˆจ ๐œ‘)}    &   ๐ถ = {๐ด, ๐ต}    โ‡’   ({โˆ…} โˆˆ ๐ด โ†’ ๐œ‘)
 
Theoremacexmidlemb 5867* Lemma for acexmid 5874. (Contributed by Jim Kingdon, 6-Aug-2019.)
๐ด = {๐‘ฅ โˆˆ {โˆ…, {โˆ…}} โˆฃ (๐‘ฅ = โˆ… โˆจ ๐œ‘)}    &   ๐ต = {๐‘ฅ โˆˆ {โˆ…, {โˆ…}} โˆฃ (๐‘ฅ = {โˆ…} โˆจ ๐œ‘)}    &   ๐ถ = {๐ด, ๐ต}    โ‡’   (โˆ… โˆˆ ๐ต โ†’ ๐œ‘)
 
Theoremacexmidlemph 5868* Lemma for acexmid 5874. (Contributed by Jim Kingdon, 6-Aug-2019.)
๐ด = {๐‘ฅ โˆˆ {โˆ…, {โˆ…}} โˆฃ (๐‘ฅ = โˆ… โˆจ ๐œ‘)}    &   ๐ต = {๐‘ฅ โˆˆ {โˆ…, {โˆ…}} โˆฃ (๐‘ฅ = {โˆ…} โˆจ ๐œ‘)}    &   ๐ถ = {๐ด, ๐ต}    โ‡’   (๐œ‘ โ†’ ๐ด = ๐ต)
 
Theoremacexmidlemab 5869* Lemma for acexmid 5874. (Contributed by Jim Kingdon, 6-Aug-2019.)
๐ด = {๐‘ฅ โˆˆ {โˆ…, {โˆ…}} โˆฃ (๐‘ฅ = โˆ… โˆจ ๐œ‘)}    &   ๐ต = {๐‘ฅ โˆˆ {โˆ…, {โˆ…}} โˆฃ (๐‘ฅ = {โˆ…} โˆจ ๐œ‘)}    &   ๐ถ = {๐ด, ๐ต}    โ‡’   (((โ„ฉ๐‘ฃ โˆˆ ๐ด โˆƒ๐‘ข โˆˆ ๐‘ฆ (๐ด โˆˆ ๐‘ข โˆง ๐‘ฃ โˆˆ ๐‘ข)) = โˆ… โˆง (โ„ฉ๐‘ฃ โˆˆ ๐ต โˆƒ๐‘ข โˆˆ ๐‘ฆ (๐ต โˆˆ ๐‘ข โˆง ๐‘ฃ โˆˆ ๐‘ข)) = {โˆ…}) โ†’ ยฌ ๐œ‘)
 
Theoremacexmidlemcase 5870* Lemma for acexmid 5874. 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 5219.

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.)

๐ด = {๐‘ฅ โˆˆ {โˆ…, {โˆ…}} โˆฃ (๐‘ฅ = โˆ… โˆจ ๐œ‘)}    &   ๐ต = {๐‘ฅ โˆˆ {โˆ…, {โˆ…}} โˆฃ (๐‘ฅ = {โˆ…} โˆจ ๐œ‘)}    &   ๐ถ = {๐ด, ๐ต}    โ‡’   (โˆ€๐‘ง โˆˆ ๐ถ โˆƒ!๐‘ฃ โˆˆ ๐‘ง โˆƒ๐‘ข โˆˆ ๐‘ฆ (๐‘ง โˆˆ ๐‘ข โˆง ๐‘ฃ โˆˆ ๐‘ข) โ†’ ({โˆ…} โˆˆ ๐ด โˆจ โˆ… โˆˆ ๐ต โˆจ ((โ„ฉ๐‘ฃ โˆˆ ๐ด โˆƒ๐‘ข โˆˆ ๐‘ฆ (๐ด โˆˆ ๐‘ข โˆง ๐‘ฃ โˆˆ ๐‘ข)) = โˆ… โˆง (โ„ฉ๐‘ฃ โˆˆ ๐ต โˆƒ๐‘ข โˆˆ ๐‘ฆ (๐ต โˆˆ ๐‘ข โˆง ๐‘ฃ โˆˆ ๐‘ข)) = {โˆ…})))
 
Theoremacexmidlem1 5871* Lemma for acexmid 5874. List the cases identified in acexmidlemcase 5870 and hook them up to the lemmas which handle each case. (Contributed by Jim Kingdon, 7-Aug-2019.)
๐ด = {๐‘ฅ โˆˆ {โˆ…, {โˆ…}} โˆฃ (๐‘ฅ = โˆ… โˆจ ๐œ‘)}    &   ๐ต = {๐‘ฅ โˆˆ {โˆ…, {โˆ…}} โˆฃ (๐‘ฅ = {โˆ…} โˆจ ๐œ‘)}    &   ๐ถ = {๐ด, ๐ต}    โ‡’   (โˆ€๐‘ง โˆˆ ๐ถ โˆƒ!๐‘ฃ โˆˆ ๐‘ง โˆƒ๐‘ข โˆˆ ๐‘ฆ (๐‘ง โˆˆ ๐‘ข โˆง ๐‘ฃ โˆˆ ๐‘ข) โ†’ (๐œ‘ โˆจ ยฌ ๐œ‘))
 
Theoremacexmidlem2 5872* Lemma for acexmid 5874. This builds on acexmidlem1 5871 by noting that every element of ๐ถ is inhabited.

(Note that ๐‘ฆ is not quite a function in the df-fun 5219 sense because it uses ordered pairs as described in opthreg 4556 rather than df-op 3602).

The set ๐ด is also found in onsucelsucexmidlem 4529.

(Contributed by Jim Kingdon, 5-Aug-2019.)

๐ด = {๐‘ฅ โˆˆ {โˆ…, {โˆ…}} โˆฃ (๐‘ฅ = โˆ… โˆจ ๐œ‘)}    &   ๐ต = {๐‘ฅ โˆˆ {โˆ…, {โˆ…}} โˆฃ (๐‘ฅ = {โˆ…} โˆจ ๐œ‘)}    &   ๐ถ = {๐ด, ๐ต}    โ‡’   (โˆ€๐‘ง โˆˆ ๐ถ โˆ€๐‘ค โˆˆ ๐‘ง โˆƒ!๐‘ฃ โˆˆ ๐‘ง โˆƒ๐‘ข โˆˆ ๐‘ฆ (๐‘ง โˆˆ ๐‘ข โˆง ๐‘ฃ โˆˆ ๐‘ข) โ†’ (๐œ‘ โˆจ ยฌ ๐œ‘))
 
Theoremacexmidlemv 5873* Lemma for acexmid 5874.

This is acexmid 5874 with additional disjoint variable conditions, most notably between ๐œ‘ and ๐‘ฅ.

(Contributed by Jim Kingdon, 6-Aug-2019.)

โˆƒ๐‘ฆโˆ€๐‘ง โˆˆ ๐‘ฅ โˆ€๐‘ค โˆˆ ๐‘ง โˆƒ!๐‘ฃ โˆˆ ๐‘ง โˆƒ๐‘ข โˆˆ ๐‘ฆ (๐‘ง โˆˆ ๐‘ข โˆง ๐‘ฃ โˆˆ ๐‘ข)    โ‡’   (๐œ‘ โˆจ ยฌ ๐œ‘)
 
Theoremacexmid 5874* 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 nonempty 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).

For this theorem stated using the df-ac 7205 and df-exmid 4196 syntaxes, see exmidac 7208. (Contributed by Jim Kingdon, 4-Aug-2019.)

โˆƒ๐‘ฆโˆ€๐‘ง โˆˆ ๐‘ฅ โˆ€๐‘ค โˆˆ ๐‘ง โˆƒ!๐‘ฃ โˆˆ ๐‘ง โˆƒ๐‘ข โˆˆ ๐‘ฆ (๐‘ง โˆˆ ๐‘ข โˆง ๐‘ฃ โˆˆ ๐‘ข)    โ‡’   (๐œ‘ โˆจ ยฌ ๐œ‘)
 
2.6.11  Operations
 
Syntaxco 5875 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 (๐ด๐น๐ต)
 
Syntaxcoprab 5876 Extend class notation to include class abstraction (class builder) of nested ordered pairs.
class {โŸจโŸจ๐‘ฅ, ๐‘ฆโŸฉ, ๐‘งโŸฉ โˆฃ ๐œ‘}
 
Syntaxcmpo 5877 Extend the definition of a class to include maps-to notation for defining an operation via a rule.
class (๐‘ฅ โˆˆ ๐ด, ๐‘ฆ โˆˆ ๐ต โ†ฆ ๐ถ)
 
Definitiondf-ov 5878 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 5911 and ovprc2 5912. 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 5879. (Contributed by NM, 28-Feb-1995.)
(๐ด๐น๐ต) = (๐นโ€˜โŸจ๐ด, ๐ตโŸฉ)
 
Definitiondf-oprab 5879* 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 5878 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 ovmpo 6010. (Contributed by NM, 12-Mar-1995.)
{โŸจโŸจ๐‘ฅ, ๐‘ฆโŸฉ, ๐‘งโŸฉ โˆฃ ๐œ‘} = {๐‘ค โˆฃ โˆƒ๐‘ฅโˆƒ๐‘ฆโˆƒ๐‘ง(๐‘ค = โŸจโŸจ๐‘ฅ, ๐‘ฆโŸฉ, ๐‘งโŸฉ โˆง ๐œ‘)}
 
Definitiondf-mpo 5880* 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 4067 for two arguments. (Contributed by NM, 17-Feb-2008.)
(๐‘ฅ โˆˆ ๐ด, ๐‘ฆ โˆˆ ๐ต โ†ฆ ๐ถ) = {โŸจโŸจ๐‘ฅ, ๐‘ฆโŸฉ, ๐‘งโŸฉ โˆฃ ((๐‘ฅ โˆˆ ๐ด โˆง ๐‘ฆ โˆˆ ๐ต) โˆง ๐‘ง = ๐ถ)}
 
Theoremoveq 5881 Equality theorem for operation value. (Contributed by NM, 28-Feb-1995.)
(๐น = ๐บ โ†’ (๐ด๐น๐ต) = (๐ด๐บ๐ต))
 
Theoremoveq1 5882 Equality theorem for operation value. (Contributed by NM, 28-Feb-1995.)
(๐ด = ๐ต โ†’ (๐ด๐น๐ถ) = (๐ต๐น๐ถ))
 
Theoremoveq2 5883 Equality theorem for operation value. (Contributed by NM, 28-Feb-1995.)
(๐ด = ๐ต โ†’ (๐ถ๐น๐ด) = (๐ถ๐น๐ต))
 
Theoremoveq12 5884 Equality theorem for operation value. (Contributed by NM, 16-Jul-1995.)
((๐ด = ๐ต โˆง ๐ถ = ๐ท) โ†’ (๐ด๐น๐ถ) = (๐ต๐น๐ท))
 
Theoremoveq1i 5885 Equality inference for operation value. (Contributed by NM, 28-Feb-1995.)
๐ด = ๐ต    โ‡’   (๐ด๐น๐ถ) = (๐ต๐น๐ถ)
 
Theoremoveq2i 5886 Equality inference for operation value. (Contributed by NM, 28-Feb-1995.)
๐ด = ๐ต    โ‡’   (๐ถ๐น๐ด) = (๐ถ๐น๐ต)
 
Theoremoveq12i 5887 Equality inference for operation value. (Contributed by NM, 28-Feb-1995.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
๐ด = ๐ต    &   ๐ถ = ๐ท    โ‡’   (๐ด๐น๐ถ) = (๐ต๐น๐ท)
 
Theoremoveqi 5888 Equality inference for operation value. (Contributed by NM, 24-Nov-2007.)
๐ด = ๐ต    โ‡’   (๐ถ๐ด๐ท) = (๐ถ๐ต๐ท)
 
Theoremoveq123i 5889 Equality inference for operation value. (Contributed by FL, 11-Jul-2010.)
๐ด = ๐ถ    &   ๐ต = ๐ท    &   ๐น = ๐บ    โ‡’   (๐ด๐น๐ต) = (๐ถ๐บ๐ท)
 
Theoremoveq1d 5890 Equality deduction for operation value. (Contributed by NM, 13-Mar-1995.)
(๐œ‘ โ†’ ๐ด = ๐ต)    โ‡’   (๐œ‘ โ†’ (๐ด๐น๐ถ) = (๐ต๐น๐ถ))
 
Theoremoveq2d 5891 Equality deduction for operation value. (Contributed by NM, 13-Mar-1995.)
(๐œ‘ โ†’ ๐ด = ๐ต)    โ‡’   (๐œ‘ โ†’ (๐ถ๐น๐ด) = (๐ถ๐น๐ต))
 
Theoremoveqd 5892 Equality deduction for operation value. (Contributed by NM, 9-Sep-2006.)
(๐œ‘ โ†’ ๐ด = ๐ต)    โ‡’   (๐œ‘ โ†’ (๐ถ๐ด๐ท) = (๐ถ๐ต๐ท))
 
Theoremoveq12d 5893 Equality deduction for operation value. (Contributed by NM, 13-Mar-1995.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
(๐œ‘ โ†’ ๐ด = ๐ต)    &   (๐œ‘ โ†’ ๐ถ = ๐ท)    โ‡’   (๐œ‘ โ†’ (๐ด๐น๐ถ) = (๐ต๐น๐ท))
 
Theoremoveqan12d 5894 Equality deduction for operation value. (Contributed by NM, 10-Aug-1995.)
(๐œ‘ โ†’ ๐ด = ๐ต)    &   (๐œ“ โ†’ ๐ถ = ๐ท)    โ‡’   ((๐œ‘ โˆง ๐œ“) โ†’ (๐ด๐น๐ถ) = (๐ต๐น๐ท))
 
Theoremoveqan12rd 5895 Equality deduction for operation value. (Contributed by NM, 10-Aug-1995.)
(๐œ‘ โ†’ ๐ด = ๐ต)    &   (๐œ“ โ†’ ๐ถ = ๐ท)    โ‡’   ((๐œ“ โˆง ๐œ‘) โ†’ (๐ด๐น๐ถ) = (๐ต๐น๐ท))
 
Theoremoveq123d 5896 Equality deduction for operation value. (Contributed by FL, 22-Dec-2008.)
(๐œ‘ โ†’ ๐น = ๐บ)    &   (๐œ‘ โ†’ ๐ด = ๐ต)    &   (๐œ‘ โ†’ ๐ถ = ๐ท)    โ‡’   (๐œ‘ โ†’ (๐ด๐น๐ถ) = (๐ต๐บ๐ท))
 
Theoremfvoveq1d 5897 Equality deduction for nested function and operation value. (Contributed by AV, 23-Jul-2022.)
(๐œ‘ โ†’ ๐ด = ๐ต)    โ‡’   (๐œ‘ โ†’ (๐นโ€˜(๐ด๐‘‚๐ถ)) = (๐นโ€˜(๐ต๐‘‚๐ถ)))
 
Theoremfvoveq1 5898 Equality theorem for nested function and operation value. Closed form of fvoveq1d 5897. (Contributed by AV, 23-Jul-2022.)
(๐ด = ๐ต โ†’ (๐นโ€˜(๐ด๐‘‚๐ถ)) = (๐นโ€˜(๐ต๐‘‚๐ถ)))
 
Theoremovanraleqv 5899* 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.)
(๐ต = ๐‘‹ โ†’ (๐œ‘ โ†” ๐œ“))    โ‡’   (๐ต = ๐‘‹ โ†’ (โˆ€๐‘ฅ โˆˆ ๐‘‰ (๐œ‘ โˆง (๐ด ยท ๐ต) = ๐ถ) โ†” โˆ€๐‘ฅ โˆˆ ๐‘‰ (๐œ“ โˆง (๐ด ยท ๐‘‹) = ๐ถ)))
 
Theoremimbrov2fvoveq 5900 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.)
(๐‘‹ = ๐‘Œ โ†’ (๐œ‘ โ†” ๐œ“))    โ‡’   (๐‘‹ = ๐‘Œ โ†’ ((๐œ‘ โ†’ (๐นโ€˜((๐บโ€˜๐‘‹) ยท ๐‘‚))๐‘…๐ด) โ†” (๐œ“ โ†’ (๐นโ€˜((๐บโ€˜๐‘Œ) ยท ๐‘‚))๐‘…๐ด)))
    < Previous  Next >

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-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12300 124 12301-12400 125 12401-12500 126 12501-12600 127 12601-12700 128 12701-12800 129 12801-12900 130 12901-13000 131 13001-13100 132 13101-13200 133 13201-13300 134 13301-13400 135 13401-13500 136 13501-13600 137 13601-13700 138 13701-13800 139 13801-13900 140 13901-14000 141 14001-14100 142 14101-14200 143 14201-14300 144 14301-14400 145 14401-14500 146 14501-14600 147 14601-14700 148 14701-14800 149 14801-14834
  Copyright terms: Public domain < Previous  Next >