P. 368 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 36701-36800   *Has distinct variable group(s)

Type	Label	Description
Statement
21.28  Mathbox for Andrew Salmon
21.28.1  Principia Mathematica * 10
Theorem	pm10.12 36701*	Theorem *10.12 in [WhiteheadRussell] p. 146. In *10, this is treated as an axiom, and the proofs in *10 are based on this theorem. (Contributed by Andrew Salmon, 17-Jun-2011.)
|- ( A. x ( ph \/ ps ) -> ( ph \/ A. x ps ) )
Theorem	pm10.14 36702	Theorem *10.14 in [WhiteheadRussell] p. 146. (Contributed by Andrew Salmon, 17-Jun-2011.)
|- ( ( A. x ph /\ A. x ps ) -> ( [ y / x ] ph /\ [ y / x ] ps ) )
Theorem	pm10.251 36703	Theorem *10.251 in [WhiteheadRussell] p. 149. (Contributed by Andrew Salmon, 17-Jun-2011.)
|- ( A. x -. ph -> -. A. x ph )
Theorem	pm10.252 36704	Theorem *10.252 in [WhiteheadRussell] p. 149. (Contributed by Andrew Salmon, 17-Jun-2011.) (New usage is discouraged.)
|- ( -. E. x ph <-> A. x -. ph )
Theorem	pm10.253 36705	Theorem *10.253 in [WhiteheadRussell] p. 149. (Contributed by Andrew Salmon, 17-Jun-2011.)
|- ( -. A. x ph <-> E. x -. ph )
Theorem	albitr 36706	Theorem *10.301 in [WhiteheadRussell] p. 151. (Contributed by Andrew Salmon, 24-May-2011.)
|- ( ( A. x ( ph <-> ps ) /\ A. x ( ps <-> ch ) ) -> A. x ( ph <-> ch ) )
Theorem	pm10.42 36707	Theorem *10.42 in [WhiteheadRussell] p. 155. (Contributed by Andrew Salmon, 17-Jun-2011.)
|- ( ( E. x ph \/ E. x ps ) <-> E. x ( ph \/ ps ) )
Theorem	pm10.52 36708*	Theorem *10.52 in [WhiteheadRussell] p. 155. (Contributed by Andrew Salmon, 24-May-2011.)
|- ( E. x ph -> ( A. x ( ph -> ps ) <-> ps ) )
Theorem	pm10.53 36709	Theorem *10.53 in [WhiteheadRussell] p. 155. (Contributed by Andrew Salmon, 24-May-2011.)
|- ( -. E. x ph -> A. x ( ph -> ps ) )
Theorem	pm10.541 36710*	Theorem *10.541 in [WhiteheadRussell] p. 155. (Contributed by Andrew Salmon, 24-May-2011.)
|- ( A. x ( ph -> ( ch \/ ps ) ) <-> ( ch \/ A. x ( ph -> ps ) ) )
Theorem	pm10.542 36711*	Theorem *10.542 in [WhiteheadRussell] p. 156. (Contributed by Andrew Salmon, 24-May-2011.)
|- ( A. x ( ph -> ( ch -> ps ) ) <-> ( ch -> A. x ( ph -> ps ) ) )
Theorem	pm10.55 36712	Theorem *10.55 in [WhiteheadRussell] p. 156. (Contributed by Andrew Salmon, 24-May-2011.)
|- ( ( E. x ( ph /\ ps ) /\ A. x ( ph -> ps ) ) <-> ( E. x ph /\ A. x ( ph -> ps ) ) )
Theorem	pm10.56 36713	Theorem *10.56 in [WhiteheadRussell] p. 156. (Contributed by Andrew Salmon, 24-May-2011.)
|- ( ( A. x ( ph -> ps ) /\ E. x ( ph /\ ch ) ) -> E. x ( ps /\ ch ) )
Theorem	pm10.57 36714	Theorem *10.57 in [WhiteheadRussell] p. 156. (Contributed by Andrew Salmon, 24-May-2011.)
|- ( A. x ( ph -> ( ps \/ ch ) ) -> ( A. x ( ph -> ps ) \/ E. x ( ph /\ ch ) ) )
21.28.2  Principia Mathematica * 11
Theorem	2alanimi 36715	Removes two universal quantifiers from a statement. (Contributed by Andrew Salmon, 24-May-2011.)
|- ( ( ph /\ ps ) -> ch )   =>    |- ( ( A. x A. y ph /\ A. x A. y ps ) -> A. x A. y ch )
Theorem	2al2imi 36716	Removes two universal quantifiers from a statement. (Contributed by Andrew Salmon, 24-May-2011.)
|- ( ph -> ( ps -> ch ) )   =>    |- ( A. x A. y ph -> ( A. x A. y ps -> A. x A. y ch ) )
Theorem	pm11.11 36717	Theorem *11.11 in [WhiteheadRussell] p. 159. (Contributed by Andrew Salmon, 17-Jun-2011.)
|- ph   =>    |- A. z A. w [ z / x ] [ w / y ] ph
Theorem	pm11.12 36718*	Theorem *11.12 in [WhiteheadRussell] p. 159. (Contributed by Andrew Salmon, 17-Jun-2011.)
|- ( A. x A. y ( ph \/ ps ) -> ( ph \/ A. x A. y ps ) )
Theorem	19.21vv 36719*	Compare Theorem *11.3 in [WhiteheadRussell] p. 161. Special case of theorem 19.21 of [Margaris] p. 90 with two quantifiers. See 19.21v 1785. (Contributed by Andrew Salmon, 24-May-2011.)
|- ( A. x A. y ( ps -> ph ) <-> ( ps -> A. x A. y ph ) )
Theorem	2alim 36720	Theorem *11.32 in [WhiteheadRussell] p. 162. Theorem 19.20 of [Margaris] p. 90 with 2 quantifiers. (Contributed by Andrew Salmon, 24-May-2011.)
|- ( A. x A. y ( ph -> ps ) -> ( A. x A. y ph -> A. x A. y ps ) )
Theorem	2albi 36721	Theorem *11.33 in [WhiteheadRussell] p. 162. Theorem 19.15 of [Margaris] p. 90 with 2 quantifiers. (Contributed by Andrew Salmon, 24-May-2011.)
|- ( A. x A. y ( ph <-> ps ) -> ( A. x A. y ph <-> A. x A. y ps ) )
Theorem	2exim 36722	Theorem *11.34 in [WhiteheadRussell] p. 162. Theorem 19.22 of [Margaris] p. 90 with 2 quantifiers. (Contributed by Andrew Salmon, 24-May-2011.)
|- ( A. x A. y ( ph -> ps ) -> ( E. x E. y ph -> E. x E. y ps ) )
Theorem	2exbi 36723	Theorem *11.341 in [WhiteheadRussell] p. 162. Theorem 19.18 of [Margaris] p. 90 with 2 quantifiers. (Contributed by Andrew Salmon, 24-May-2011.)
|- ( A. x A. y ( ph <-> ps ) -> ( E. x E. y ph <-> E. x E. y ps ) )
Theorem	spsbce-2 36724	Theorem *11.36 in [WhiteheadRussell] p. 162. (Contributed by Andrew Salmon, 24-May-2011.)
|- ( [ z / x ] [ w / y ] ph -> E. x E. y ph )
Theorem	19.33-2 36725	Theorem *11.421 in [WhiteheadRussell] p. 163. Theorem 19.33 of [Margaris] p. 90 with 2 quantifiers. (Contributed by Andrew Salmon, 24-May-2011.)
|- ( ( A. x A. y ph \/ A. x A. y ps ) -> A. x A. y ( ph \/ ps ) )
Theorem	19.36vv 36726*	Theorem *11.43 in [WhiteheadRussell] p. 163. Theorem 19.36 of [Margaris] p. 90 with 2 quantifiers. (Contributed by Andrew Salmon, 25-May-2011.)
|- ( E. x E. y ( ph -> ps ) <-> ( A. x A. y ph -> ps ) )
Theorem	19.31vv 36727*	Theorem *11.44 in [WhiteheadRussell] p. 163. Theorem 19.31 of [Margaris] p. 90 with 2 quantifiers. (Contributed by Andrew Salmon, 24-May-2011.)
|- ( A. x A. y ( ph \/ ps ) <-> ( A. x A. y ph \/ ps ) )
Theorem	19.37vv 36728*	Theorem *11.46 in [WhiteheadRussell] p. 164. Theorem 19.37 of [Margaris] p. 90 with 2 quantifiers. (Contributed by Andrew Salmon, 24-May-2011.)
|- ( E. x E. y ( ps -> ph ) <-> ( ps -> E. x E. y ph ) )
Theorem	19.28vv 36729*	Theorem *11.47 in [WhiteheadRussell] p. 164. Theorem 19.28 of [Margaris] p. 90 with 2 quantifiers. (Contributed by Andrew Salmon, 24-May-2011.)
|- ( A. x A. y ( ps /\ ph ) <-> ( ps /\ A. x A. y ph ) )
Theorem	pm11.52 36730	Theorem *11.52 in [WhiteheadRussell] p. 164. (Contributed by Andrew Salmon, 24-May-2011.)
|- ( E. x E. y ( ph /\ ps ) <-> -. A. x A. y ( ph -> -. ps ) )
Theorem	2exanali 36731	Theorem *11.521 in [WhiteheadRussell] p. 164. (Contributed by Andrew Salmon, 24-May-2011.)
|- ( -. E. x E. y ( ph /\ -. ps ) <-> A. x A. y ( ph -> ps ) )
Theorem	aaanv 36732*	Theorem *11.56 in [WhiteheadRussell] p. 165. Special case of aaan 2054. (Contributed by Andrew Salmon, 24-May-2011.)
|- ( ( A. x ph /\ A. y ps ) <-> A. x A. y ( ph /\ ps ) )
Theorem	pm11.57 36733*	Theorem *11.57 in [WhiteheadRussell] p. 165. (Contributed by Andrew Salmon, 24-May-2011.)
|- ( A. x ph <-> A. x A. y ( ph /\ [ y / x ] ph ) )
Theorem	pm11.58 36734*	Theorem *11.58 in [WhiteheadRussell] p. 165. (Contributed by Andrew Salmon, 24-May-2011.)
|- ( E. x ph <-> E. x E. y ( ph /\ [ y / x ] ph ) )
Theorem	pm11.59 36735*	Theorem *11.59 in [WhiteheadRussell] p. 165. (Contributed by Andrew Salmon, 25-May-2011.)
|- ( A. x ( ph -> ps ) -> A. y A. x ( ( ph /\ [ y / x ] ph ) -> ( ps /\ [ y / x ] ps ) ) )
Theorem	pm11.6 36736*	Theorem *11.6 in [WhiteheadRussell] p. 165. (Contributed by Andrew Salmon, 25-May-2011.)
|- ( E. x ( E. y ( ph /\ ps ) /\ ch ) <-> E. y ( E. x ( ph /\ ch ) /\ ps ) )
Theorem	pm11.61 36737*	Theorem *11.61 in [WhiteheadRussell] p. 166. (Contributed by Andrew Salmon, 24-May-2011.)
|- ( E. y A. x ( ph -> ps ) -> A. x ( ph -> E. y ps ) )
Theorem	pm11.62 36738*	Theorem *11.62 in [WhiteheadRussell] p. 166. Importation combined with the rearrangement with quantifiers. (Contributed by Andrew Salmon, 24-May-2011.)
|- ( A. x A. y ( ( ph /\ ps ) -> ch ) <-> A. x ( ph -> A. y ( ps -> ch ) ) )
Theorem	pm11.63 36739	Theorem *11.63 in [WhiteheadRussell] p. 166. (Contributed by Andrew Salmon, 24-May-2011.)
|- ( -. E. x E. y ph -> A. x A. y ( ph -> ps ) )
Theorem	pm11.7 36740	Theorem *11.7 in [WhiteheadRussell] p. 166. (Contributed by Andrew Salmon, 24-May-2011.)
|- ( E. x E. y ( ph \/ ph ) <-> E. x E. y ph )
Theorem	pm11.71 36741*	Theorem *11.71 in [WhiteheadRussell] p. 166. (Contributed by Andrew Salmon, 24-May-2011.)
|- ( ( E. x ph /\ E. y ch ) -> ( ( A. x ( ph -> ps ) /\ A. y ( ch -> th ) ) <-> A. x A. y ( ( ph /\ ch ) -> ( ps /\ th ) ) ) )
21.28.3  Predicate Calculus
Theorem	sbeqal1 36742*	If x = y always implies x = z, then y = z is true. (Contributed by Andrew Salmon, 2-Jun-2011.)
|- ( A. x ( x = y -> x = z ) -> y = z )
Theorem	sbeqal1i 36743*	Suppose you know x = y implies x = z, assuming x and z are distinct. Then, y = z. (Contributed by Andrew Salmon, 3-Jun-2011.)
|- ( x = y -> x = z )   =>    |- y = z
Theorem	sbeqal2i 36744*	If x = y implies x = z, then we can infer z = y. (Contributed by Andrew Salmon, 3-Jun-2011.)
|- ( x = y -> x = z )   =>    |- z = y
Theorem	sbeqalbi 36745*	When both x and z and y and z are both distinct, then the converse of sbeqal1 holds as well. (Contributed by Andrew Salmon, 2-Jun-2011.)
|- ( x = y <-> A. z ( z = x -> z = y ) )
Theorem	axc5c4c711 36746	Proof of a theorem that can act as a sole axiom for pure predicate calculus with ax-gen 1668 as the inference rule. This proof extends the idea of axc5c711 32483 and related theorems. (Contributed by Andrew Salmon, 14-Jul-2011.)
|- ( ( A. x A. y -. A. x A. y ( A. y ph -> ps ) -> ( ph -> A. y ( A. y ph -> ps ) ) ) -> ( A. y ph -> A. y ps ) )
Theorem	axc5c4c711toc5 36747	Re-derivation of sp 1936 from axc5c4c711 36746. Note that ax6 2094 is used for the re-derivation. (Contributed by Andrew Salmon, 14-Jul-2011.) Revised to use ax6v 1805 instead of ax6 2094, so that this re-derivation requires only ax6v 1805 and propositional calculus. (Revised by BJ, 14-Sep-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( A. x ph -> ph )
Theorem	axc5c4c711toc4 36748	Re-derivation of axc4 1937 from axc5c4c711 36746. Note that only propositional calculus is required for the re-derivation. (Contributed by Andrew Salmon, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( A. x ( A. x ph -> ps ) -> ( A. x ph -> A. x ps ) )
Theorem	axc5c4c711toc7 36749	Re-derivation of axc7 1938 from axc5c4c711 36746. Note that neither axc7 1938 nor ax-11 1919 are required for the re-derivation. (Contributed by Andrew Salmon, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( -. A. x -. A. x ph -> ph )
Theorem	axc5c4c711to11 36750	Re-derivation of ax-11 1919 from axc5c4c711 36746. Note that ax-11 1919 is not required for the re-derivation. (Contributed by Andrew Salmon, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( A. x A. y ph -> A. y A. x ph )
Theorem	axc11next 36751*	This theorem shows that, given axext4 2434, we can derive a version of axc11n 2142. However, it is weaker than axc11n 2142 because it has a distinct variable requirement. (Contributed by Andrew Salmon, 16-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( A. x x = z -> A. z z = x )
21.28.4  Principia Mathematica * 13 and * 14
Theorem	pm13.13a 36752	One result of theorem *13.13 in [WhiteheadRussell] p. 178. A note on the section - to make the theorems more usable, and because inequality is notation for set theory (it is not defined in the predicate calculus section), this section will use classes instead of sets. (Contributed by Andrew Salmon, 3-Jun-2011.)
|- ( ( ph /\ x = A ) -> [. A / x ]. ph )
Theorem	pm13.13b 36753	Theorem *13.13 in [WhiteheadRussell] p. 178 with different variable substitution. (Contributed by Andrew Salmon, 3-Jun-2011.)
|- ( ( [. A / x ]. ph /\ x = A ) -> ph )
Theorem	pm13.14 36754	Theorem *13.14 in [WhiteheadRussell] p. 178. (Contributed by Andrew Salmon, 3-Jun-2011.)
|- ( ( [. A / x ]. ph /\ -. ph ) -> x =/= A )
Theorem	pm13.192 36755*	Theorem *13.192 in [WhiteheadRussell] p. 179. (Contributed by Andrew Salmon, 3-Jun-2011.) (Revised by NM, 4-Jan-2017.)
|- ( E. y ( A. x ( x = A <-> x = y ) /\ ph ) <-> [. A / y ]. ph )
Theorem	pm13.193 36756	Theorem *13.193 in [WhiteheadRussell] p. 179. (Contributed by Andrew Salmon, 3-Jun-2011.)
|- ( ( ph /\ x = y ) <-> ( [ y / x ] ph /\ x = y ) )
Theorem	pm13.194 36757	Theorem *13.194 in [WhiteheadRussell] p. 179. (Contributed by Andrew Salmon, 3-Jun-2011.)
|- ( ( ph /\ x = y ) <-> ( [ y / x ] ph /\ ph /\ x = y ) )
Theorem	pm13.195 36758*	Theorem *13.195 in [WhiteheadRussell] p. 179. This theorem is very similar to sbc5 3291. (Contributed by Andrew Salmon, 3-Jun-2011.) (Revised by NM, 4-Jan-2017.)
|- ( E. y ( y = A /\ ph ) <-> [. A / y ]. ph )
Theorem	pm13.196a 36759*	Theorem *13.196 in [WhiteheadRussell] p. 179. The only difference is the position of the substituted variable. (Contributed by Andrew Salmon, 3-Jun-2011.)
|- ( -. ph <-> A. y ( [ y / x ] ph -> y =/= x ) )
Theorem	2sbc6g 36760*	Theorem *13.21 in [WhiteheadRussell] p. 179. (Contributed by Andrew Salmon, 3-Jun-2011.)
|- ( ( A e. C /\ B e. D ) -> ( A. z A. w ( ( z = A /\ w = B ) -> ph ) <-> [. A / z ]. [. B / w ]. ph ) )
Theorem	2sbc5g 36761*	Theorem *13.22 in [WhiteheadRussell] p. 179. (Contributed by Andrew Salmon, 3-Jun-2011.)
|- ( ( A e. C /\ B e. D ) -> ( E. z E. w ( ( z = A /\ w = B ) /\ ph ) <-> [. A / z ]. [. B / w ]. ph ) )
Theorem	iotain 36762	Equivalence between two different forms of iota. (Contributed by Andrew Salmon, 15-Jul-2011.)
|- ( E! x ph -> |^| { x | ph } = ( iota x ph ) )
Theorem	iotaexeu 36763	The iota class exists. This theorem does not require ax-nul 4533 for its proof. (Contributed by Andrew Salmon, 11-Jul-2011.)
|- ( E! x ph -> ( iota x ph ) e. _V )
Theorem	iotasbc 36764*	Definition *14.01 in [WhiteheadRussell] p. 184. In Principia Mathematica, Russell and Whitehead define iota in terms of a function of ( iota x ph ). Their definition differs in that a function of ( iota x ph ) evaluates to "false" when there isn't a single x that satisfies ph. (Contributed by Andrew Salmon, 11-Jul-2011.)
|- ( E! x ph -> ( [. ( iota x ph ) / y ]. ps <-> E. y ( A. x ( ph <-> x = y ) /\ ps ) ) )
Theorem	iotasbc2 36765*	Theorem *14.111 in [WhiteheadRussell] p. 184. (Contributed by Andrew Salmon, 11-Jul-2011.)
|- ( ( E! x ph /\ E! x ps ) -> ( [. ( iota x ph ) / y ]. [. ( iota x ps ) / z ]. ch <-> E. y E. z ( A. x ( ph <-> x = y ) /\ A. x ( ps <-> x = z ) /\ ch ) ) )
Theorem	pm14.12 36766*	Theorem *14.12 in [WhiteheadRussell] p. 184. (Contributed by Andrew Salmon, 11-Jul-2011.)
|- ( E! x ph -> A. x A. y ( ( ph /\ [. y / x ]. ph ) -> x = y ) )
Theorem	pm14.122a 36767*	Theorem *14.122 in [WhiteheadRussell] p. 185. (Contributed by Andrew Salmon, 9-Jun-2011.)
|- ( A e. V -> ( A. x ( ph <-> x = A ) <-> ( A. x ( ph -> x = A ) /\ [. A / x ]. ph ) ) )
Theorem	pm14.122b 36768*	Theorem *14.122 in [WhiteheadRussell] p. 185. (Contributed by Andrew Salmon, 9-Jun-2011.)
|- ( A e. V -> ( ( A. x ( ph -> x = A ) /\ [. A / x ]. ph ) <-> ( A. x ( ph -> x = A ) /\ E. x ph ) ) )
Theorem	pm14.122c 36769*	Theorem *14.122 in [WhiteheadRussell] p. 185. (Contributed by Andrew Salmon, 9-Jun-2011.)
|- ( A e. V -> ( A. x ( ph <-> x = A ) <-> ( A. x ( ph -> x = A ) /\ E. x ph ) ) )
Theorem	pm14.123a 36770*	Theorem *14.123 in [WhiteheadRussell] p. 185. (Contributed by Andrew Salmon, 9-Jun-2011.)
|- ( ( A e. V /\ B e. W ) -> ( A. z A. w ( ph <-> ( z = A /\ w = B ) ) <-> ( A. z A. w ( ph -> ( z = A /\ w = B ) ) /\ [. A / z ]. [. B / w ]. ph ) ) )
Theorem	pm14.123b 36771*	Theorem *14.123 in [WhiteheadRussell] p. 185. (Contributed by Andrew Salmon, 9-Jun-2011.)
|- ( ( A e. V /\ B e. W ) -> ( ( A. z A. w ( ph -> ( z = A /\ w = B ) ) /\ [. A / z ]. [. B / w ]. ph ) <-> ( A. z A. w ( ph -> ( z = A /\ w = B ) ) /\ E. z E. w ph ) ) )
Theorem	pm14.123c 36772*	Theorem *14.123 in [WhiteheadRussell] p. 185. (Contributed by Andrew Salmon, 9-Jun-2011.)
|- ( ( A e. V /\ B e. W ) -> ( A. z A. w ( ph <-> ( z = A /\ w = B ) ) <-> ( A. z A. w ( ph -> ( z = A /\ w = B ) ) /\ E. z E. w ph ) ) )
Theorem	pm14.18 36773	Theorem *14.18 in [WhiteheadRussell] p. 189. (Contributed by Andrew Salmon, 11-Jul-2011.)
|- ( E! x ph -> ( A. x ps -> [. ( iota x ph ) / x ]. ps ) )
Theorem	iotaequ 36774*	Theorem *14.2 in [WhiteheadRussell] p. 189. (Contributed by Andrew Salmon, 11-Jul-2011.)
|- ( iota x x = y ) = y
Theorem	iotavalb 36775*	Theorem *14.202 in [WhiteheadRussell] p. 189. A biconditional version of iotaval 5556. (Contributed by Andrew Salmon, 11-Jul-2011.)
|- ( E! x ph -> ( A. x ( ph <-> x = y ) <-> ( iota x ph ) = y ) )
Theorem	iotasbc5 36776*	Theorem *14.205 in [WhiteheadRussell] p. 190. (Contributed by Andrew Salmon, 11-Jul-2011.)
|- ( E! x ph -> ( [. ( iota x ph ) / y ]. ps <-> E. y ( y = ( iota x ph ) /\ ps ) ) )
Theorem	pm14.24 36777*	Theorem *14.24 in [WhiteheadRussell] p. 191. (Contributed by Andrew Salmon, 12-Jul-2011.)
|- ( E! x ph -> A. y ( [. y / x ]. ph <-> y = ( iota x ph ) ) )
Theorem	iotavalsb 36778*	Theorem *14.242 in [WhiteheadRussell] p. 192. (Contributed by Andrew Salmon, 11-Jul-2011.)
|- ( A. x ( ph <-> x = y ) -> ( [. y / z ]. ps <-> [. ( iota x ph ) / z ]. ps ) )
Theorem	sbiota1 36779	Theorem *14.25 in [WhiteheadRussell] p. 192. (Contributed by Andrew Salmon, 12-Jul-2011.)
|- ( E! x ph -> ( A. x ( ph -> ps ) <-> [. ( iota x ph ) / x ]. ps ) )
Theorem	sbaniota 36780	Theorem *14.26 in [WhiteheadRussell] p. 192. (Contributed by Andrew Salmon, 12-Jul-2011.)
|- ( E! x ph -> ( E. x ( ph /\ ps ) <-> [. ( iota x ph ) / x ]. ps ) )
Theorem	eubi 36781	Theorem *14.271 in [WhiteheadRussell] p. 192. (Contributed by Andrew Salmon, 11-Jul-2011.)
|- ( A. x ( ph <-> ps ) -> ( E! x ph <-> E! x ps ) )
Theorem	iotasbcq 36782	Theorem *14.272 in [WhiteheadRussell] p. 193. (Contributed by Andrew Salmon, 11-Jul-2011.)
|- ( A. x ( ph <-> ps ) -> ( [. ( iota x ph ) / y ]. ch <-> [. ( iota x ps ) / y ]. ch ) )
21.28.5  Set Theory
Theorem	elnev 36783*	Any set that contains one element less than the universe is not equal to it. (Contributed by Andrew Salmon, 16-Jun-2011.)
|- ( A e. _V <-> { x | -. x = A } =/= _V )
Theorem	rusbcALT 36784	A version of Russell's paradox which is proven using proper substitution. (Contributed by Andrew Salmon, 18-Jun-2011.) (New usage is discouraged.) (Proof modification is discouraged.)
|- { x | x e/ x } e/ _V
Theorem	compel 36785	Equivalence between two ways of saying "is a member of the complement of A." (Contributed by Andrew Salmon, 15-Jul-2011.)
|- ( x e. ( _V \ A ) <-> -. x e. A )
Theorem	compeq 36786*	Equality between two ways of saying "the complement of A." (Contributed by Andrew Salmon, 15-Jul-2011.)
|- ( _V \ A ) = { x | -. x e. A }
Theorem	compne 36787	The complement of A is not equal to A. (Contributed by Andrew Salmon, 15-Jul-2011.)
|- ( _V \ A ) =/= A
Theorem	compab 36788	Two ways of saying "the complement of a class abstraction". (Contributed by Andrew Salmon, 15-Jul-2011.) (Proof shortened by Mario Carneiro, 11-Dec-2016.)
|- ( _V \ { z | ph } ) = { z | -. ph }
Theorem	conss34 36789	Contrpositive law for subsets. (Contributed by Andrew Salmon, 15-Jul-2011.)
|- ( A C_ B <-> ( _V \ B ) C_ ( _V \ A ) )
Theorem	conss2 36790	Contrapositive law for subsets. (Contributed by Andrew Salmon, 15-Jul-2011.)
|- ( A C_ ( _V \ B ) <-> B C_ ( _V \ A ) )
Theorem	conss1 36791	Contrapositive law for subsets. (Contributed by Andrew Salmon, 15-Jul-2011.)
|- ( ( _V \ A ) C_ B <-> ( _V \ B ) C_ A )
Theorem	ralbidar 36792	More general form of ralbida 2820. (Contributed by Andrew Salmon, 25-Jul-2011.)
|- ( ph -> A. x e. A ph )   &    |- ( ( ph /\ x e. A ) -> ( ps <-> ch ) )   =>    |- ( ph -> ( A. x e. A ps <-> A. x e. A ch ) )
Theorem	rexbidar 36793	More general form of rexbida 2895. (Contributed by Andrew Salmon, 25-Jul-2011.)
|- ( ph -> A. x e. A ph )   &    |- ( ( ph /\ x e. A ) -> ( ps <-> ch ) )   =>    |- ( ph -> ( E. x e. A ps <-> E. x e. A ch ) )
Theorem	dropab1 36794	Theorem to aid use of the distinctor reduction theorem with ordered pair class abstraction. (Contributed by Andrew Salmon, 25-Jul-2011.)
|- ( A. x x = y -> { <. x , z >. | ph } = { <. y , z >. | ph } )
Theorem	dropab2 36795	Theorem to aid use of the distinctor reduction theorem with ordered pair class abstraction. (Contributed by Andrew Salmon, 25-Jul-2011.)
|- ( A. x x = y -> { <. z , x >. | ph } = { <. z , y >. | ph } )
Theorem	ipo0 36796	If the identity relation partially orders any class, then that class is the null class. (Contributed by Andrew Salmon, 25-Jul-2011.)
|- ( _I Po A <-> A = (/) )
Theorem	ifr0 36797	A class that is founded by the identity relation is null. (Contributed by Andrew Salmon, 25-Jul-2011.)
|- ( _I Fr A <-> A = (/) )
Theorem	ordpss 36798	ordelpss 5450 with an antecedent removed. (Contributed by Andrew Salmon, 25-Jul-2011.)
|- ( Ord B -> ( A e. B -> A C. B ) )
Theorem	fvsb 36799*	Explicit substitution of a value of a function into a wff. (Contributed by Andrew Salmon, 1-Aug-2011.)
|- ( E! y A F y -> ( [. ( F ` A ) / x ]. ph <-> E. x ( A. y ( A F y <-> y = x ) /\ ph ) ) )
Theorem	fveqsb 36800*	Implicit substitution of a value of a function into a wff. (Contributed by Andrew Salmon, 1-Aug-2011.)
|- ( x = ( F ` A ) -> ( ph <-> ps ) )   &    |- F/ x ps   =>    |- ( E! y A F y -> ( ps <-> E. x ( A. y ( A F y <-> y = x ) /\ ph ) ) )