mmtheorems138 - Metamath Proof Explorer

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-14900 150 14901-15000 151 15001-15100 152 15101-15200 153 15201-15300 154 15301-15400 155 15401-15500 156 15501-15600 157 15601-15700 158 15701-15800 159 15801-15900 160 15901-16000 161 16001-16100 162 16101-16200 163 16201-16300 164 16301-16400 165 16401-16500 166 16501-16600 167 16601-16700 168 16701-16800 169 16801-16900 170 16901-17000 171 17001-17100 172 17101-17200 173 17201-17300 174 17301-17400 175 17401-17500 176 17501-17600 177 17601-17700 178 17701-17800 179 17801-17900 180 17901-18000 181 18001-18100 182 18101-18200 183 18201-18300 184 18301-18400 185 18401-18500 186 18501-18600 187 18601-18700 188 18701-18800 189 18801-18900 190 18901-19000 191 19001-19026

Statement List for Metamath Proof Explorer - 13701-13800 - Page 138 of 191

Type	Label	Description
Statement
Theorem	bnj1120 13701	First-order logic and set theory.
|- (((A = B -> ps) /\ (A =/= B -> ps)) -> ps)
Theorem	bnj1109 13702	First-order logic and set theory.
|- E.x((A =/= B /\ ph) -> ps)   &   |- ((A = B /\ ph) -> ps)   =>   |- E.x(ph -> ps)
Theorem	bnj1126 13703	First-order logic and set theory.
|- (ph -> ps)   &   |- E.x(ph -> (ps' <-> ps))   =>   |- E.x(ph -> ps')
Theorem	bnj1130 13704	First-order logic and set theory.
|- (ph -> ps)   &   |- E.x(ph -> (ps <-> ch))   =>   |- E.x(ph -> ch)
Theorem	bnj1131 13705	First-order logic and set theory.
|- (ph -> A.xph)   &   |- E.xph   =>   |- ph
Theorem	bnj1135 13706	First-order logic and set theory.
|- (ph <-> A.x e. A (ps -> ch))   &   |- (ch <-> (th -> ta))   =>   |- (ph <-> A.x e. A (ps -> (th -> ta)))
Theorem	bnj1138 13707	First-order logic and set theory.
|- A = (B u. C)   =>   |- (X e. A <-> (X e. B \/ X e. C))
Theorem	bnj1139 13708	First-order logic and set theory.
|- (ph <-> (ps \/ ch))   &   |- ((th /\ ta /\ ps) -> et)   &   |- ((th /\ ta /\ ch) -> et)   =>   |- ((th /\ ta /\ ph) -> et)
Theorem	bnj1140 13709	First-order logic and set theory.
|- ((ph /\ ps) -> A C_ B)   =>   |- ((ph /\ ps /\ X e. A) -> X e. B)
Theorem	bnj1141 13710	First-order logic and set theory.
|- (ph -> A C_ B)   &   |- B C_ C   =>   |- (ph -> A C_ C)
Theorem	bnj1142 13711	First-order logic and set theory.
|- (ph -> A.x(x e. A -> ps))   =>   |- (ph -> A.x e. A ps)
Theorem	bnj1144 13712	First-order logic and set theory.
|- (A = (/) -> U_x e. A B = (/))
Theorem	bnj1143 13713	First-order logic and set theory.
|- U_x e. A B C_ B
Theorem	bnj1146 13714	First-order logic and set theory.
|- (y e. A -> A.x y e. A)   =>   |- U_x e. A B C_ B
Theorem	bnj1149 13715	First-order logic and set theory.
|- (ph -> A e. _V)   &   |- (ph -> B e. _V)   =>   |- (ph -> (A u. B) e. _V)
Theorem	bnj1150 13716	First-order logic and set theory.
|- (ph -> A C_ C)   &   |- (ph -> B C_ C)   =>   |- (ph -> (A u. B) C_ C)
Theorem	bnj1153 13717	First-order logic and set theory.
|- (ph -> X e. A)   &   |- (ph -> X e. B)   =>   |- (ph -> X e. (A i^i B))
Theorem	bnj1155 13718	First-order logic and set theory.
|- (ph -> A.x(ps <-> ch))   =>   |- (ph -> (A.xps <-> A.xch))
Theorem	bnj1156 13719	First-order logic and set theory.
|- (ph -> (A.x(x e. A -> ps) <-> A.y(y e. B -> ch)))   =>   |- (ph -> (A.x e. A ps <-> A.y e. B ch))
Theorem	bnj1157 13720	First-order logic and set theory.
|- (ph -> A.x(ps <-> ch))   =>   |- (ph -> (E.xps <-> E.xch))
Theorem	bnj1158 13721	First-order logic and set theory.
|- (ph -> (E.x(x e. A /\ ps) <-> E.y(y e. B /\ ch)))   =>   |- (ph -> (E.x e. A ps <-> E.y e. B ch))
Theorem	bnj1159 13722	First-order logic and set theory.
|- (ph -> E.x e. A A.y e. B ps)   =>   |- (ph -> E.x e. A A.y(y e. B -> ps))
Theorem	bnj1160 13723	First-order logic and set theory.
|- (ph -> E.x e. A A.y(y e. B -> ps))   =>   |- (ph -> E.x(x e. A /\ A.y(y e. B -> ps)))
Theorem	bnj1161 13724	First-order logic and set theory.
|- (ph -> E.x(x e. A /\ A.y(y e. B -> ps)))   =>   |- (ph -> E.xA.y(x e. A /\ (y e. B -> ps)))
Theorem	bnj1162 13725	First-order logic and set theory.
|- (ph -> E.xA.y(x e. A /\ (y e. B -> ps)))   =>   |- E.xA.y(ph -> (x e. A /\ (y e. B -> ps)))
Theorem	bnj1163 13726	First-order logic and set theory.
|- (ph <-> (ps /\ ch /\ (th /\ ta)))   &   |- (et <-> (ps /\ ch /\ th))   =>   |- (ph <-> (et /\ ta))
Theorem	bnj1164 13727	First-order logic and set theory.
|- ((X e. A /\ -. X e. (A i^i B)) -> -. X e. B)
Theorem	bnj1165 13728	First-order logic and set theory.
|- (((ph -> ps) /\ (ph -> (ps -> ch))) -> (ph -> ch))
Theorem	bnj1166 13729	First-order logic and set theory.
|- E.xA.y(ph -> (ps /\ (ch -> -. th)))   =>   |- E.xA.y(ph -> (ps /\ (th -> -. ch)))
Theorem	bnj1167 13730	First-order logic and set theory.
|- E.xA.y(ph -> (ps /\ ch))   =>   |- E.xA.y(ph -> (ps /\ (th -> ch)))
Theorem	bnj1168 13731	First-order logic and set theory.
|- E.xA.y((ph /\ ps) -> (ch /\ (th -> ta)))   =>   |- E.xA.y((ph /\ ps) -> (ph /\ ps /\ ch /\ (th -> ta)))
Theorem	bnj1169 13732	First-order logic and set theory.
|- (ph -> ps)   =>   |- (ph -> ((ps /\ ch /\ th) <-> (ch /\ th)))
Theorem	bnj1170 13733	First-order logic and set theory.
|- (ph -> ps)   =>   |- (ph -> ((ps /\ ch) <-> ch))
Theorem	bnj1181 13734	First-order logic and set theory.
|- E.xA.y(ph -> ps)   =>   |- E.x(ph -> A.yps)
Theorem	bnj1182 13735	First-order logic and set theory.
|- (ph -> E.xA.y(ps /\ ch))   =>   |- (ph -> E.x(ps /\ A.ych))
Theorem	bnj1183 13736	First-order logic and set theory.
|- (ph -> E.x(ps /\ A.y(y e. A -> ch)))   =>   |- (ph -> E.x(ps /\ A.y e. A ch))
Theorem	bnj1184 13737	First-order logic and set theory.
|- (ph -> E.x(x e. B /\ A.y e. A ch))   =>   |- (ph -> E.x e. B A.y e. A ch)
Theorem	bnj1185 13738	First-order logic and set theory.
|- (ph -> E.z e. B A.w e. B -. wRz)   =>   |- (ph -> E.x e. B A.y e. B -. yRx)
Theorem	bnj1191 13739	First-order logic and set theory.
|- (ph <-> (ps /\ ch /\ A =/= (/)))   =>   |- (ph -> E.x x e. A)
Theorem	bnj1192 13740	First-order logic and set theory.
|- (ch <-> ch')   =>   |- ((ph /\ ps /\ ch) -> (ps /\ ch'))
Theorem	bnj1193 13741	First-order logic and set theory.
|- (ph -> ps)   =>   |- (ph -> E.xps)
Theorem	bnj1194 13742	First-order logic and set theory.
|- (ph <-> A.x e. A -. ps)   =>   |- (-. ph <-> E.x e. A ps)
Theorem	bnj1196 13743	First-order logic and set theory.
|- (ph -> E.x e. A ps)   =>   |- (ph -> E.x(x e. A /\ ps))
Theorem	bnj1197 13744	First-order logic and set theory.
|- (ph -> (ps /\ E.x(ch /\ th)))   =>   |- (ph -> E.x(ps /\ ch /\ th))
Theorem	bnj1198 13745	First-order logic and set theory.
|- (ph -> E.xps)   &   |- (ps' <-> ps)   =>   |- (ph -> E.xps')
Theorem	bnj1199 13746	First-order logic and set theory.
|- (ph -> (ps /\ E.xch))   =>   |- (ph -> E.x(ps /\ ch))
Theorem	bnj1195 13747	First-order logic and set theory.
|- (ps <-> (th /\ y e. B /\ ta))   &   |- (ch <-> E.y e. B ta)   =>   |- ((ph /\ th /\ ch) -> E.y(ph /\ ps))
Theorem	bnj1200 13748	First-order logic and set theory.
|- ((ph /\ ps /\ ch) -> th)   &   |- ((ph /\ ps /\ -. ch) -> th)   =>   |- ((ph /\ ps) -> th)
Theorem	bnj1201 13749	First-order logic and set theory.
|- (ph -> E.xE.xps)   =>   |- (ph -> E.xps)
Theorem	bnj1202 13750	First-order logic and set theory.
|- (ph -> E.xE.x e. A ps)   =>   |- (ph -> E.x e. A ps)
Theorem	bnj1206OLD 13751	First-order logic and set theory. (Moved into main set.mm as simp1bi 1135 and may be deleted by mathbox owner, JBN. --NM 9-Sep-2011.)
|- (ph <-> (ps /\ ch /\ th))   =>   |- (ph -> ps)
Theorem	bnj1207 13752	First-order logic and set theory.
|- B = {x e. A | ph}   =>   |- (ps -> B C_ A)
Theorem	bnj1208 13753	First-order logic and set theory.
|- B = {x e. A | ph}   &   |- (ch <-> (ps /\ th /\ E.x e. A ph))   =>   |- (ch -> B =/= (/))
Theorem	bnj1209 13754	First-order logic and set theory.
|- (ch -> E.x e. B ph)   &   |- (th <-> (ch /\ x e. B /\ ph))   =>   |- (ch -> E.xth)
Theorem	bnj1211 13755	First-order logic and set theory.
|- (ph -> A.x e. A ps)   =>   |- (ph -> A.x(x e. A -> ps))
Theorem	bnj1210 13756	First-order logic and set theory.
|- ((x e. A /\ ps /\ A.x e. A (ps -> ph)) -> ph)
Theorem	bnj1213 13757	First-order logic and set theory.
|- A C_ B   &   |- (th -> x e. A)   =>   |- (th -> x e. B)
Theorem	bnj1212 13758	First-order logic and set theory.
|- B = {x e. A | ph}   &   |- (th <-> (ch /\ x e. B /\ ta))   =>   |- (th -> x e. A)
Theorem	bnj1214 13759	First-order logic and set theory.
|- ((y e. A /\ yRx /\ A.y e. B -. yRx) -> (y e. A /\ -. y e. B))
Theorem	bnj1216 13760	First-order logic and set theory.
|- {x e. A | ph} = {y e. A | [y / x]ph}
Theorem	bnj1217 13761	First-order logic and set theory.
|- (ph -> -. -. ps)   =>   |- (ph -> ps)
Theorem	bnj1215 13762	First-order logic and set theory.
|- B = {x e. A | -. ph}   &   |- (ps -> (y e. A /\ -. y e. B))   =>   |- (ps -> [y / x]ph)
Theorem	bnj1218 13763	First-order logic and set theory.
|- ((y e. A /\ ta /\ A.y e. B ch) -> th)   &   |- (ps <-> A.y e. A (ta -> th))   =>   |- (A.y e. B ch -> ps)
Theorem	bnj1219 13764	First-order logic and set theory.
|- (ch <-> (ph /\ ps /\ ze))   &   |- (th <-> (ch /\ ta /\ et))   =>   |- (th -> ps)
Theorem	bnj1220 13765	First-order logic and set theory.
|- B = {x e. A | -. ph}   =>   |- (x e. B -> -. ph)
Theorem	bnj1222 13766	First-order logic and set theory.
|- (A.x(ps \/ -. ps) <-> -. E.x(ps /\ -. ps))
Theorem	bnj1221 13767	First-order logic and set theory.
|- (ph -> E.x(ps /\ -. ps))   =>   |- -. ph
Theorem	bnj1225 13768	First-order logic and set theory.
|- -. (ph /\ ps)   =>   |- (-. ph \/ -. ps)
Theorem	bnj1226OLD 13769	First-order logic and set theory. (Moved into main set.mm as imorri 355 and may be deleted by mathbox owner, JBN. --NM 17-Aug-2011.)
|- (-. ph \/ ps)   =>   |- (ph -> ps)
Theorem	bnj1224 13770	First-order logic and set theory.
|- -. (th /\ ta /\ et)   =>   |- ((th /\ ta) -> -. et)
Theorem	bnj1227 13771	First-order logic and set theory.
|- (ph -> -. E.x e. A -. ps)   =>   |- (ph -> A.x e. A ps)
Theorem	bnj1223 13772	First-order logic and set theory.
|- (ch <-> (th /\ ta /\ E.x e. A -. ph))   &   |- -. ch   =>   |- ((th /\ ta) -> A.x e. A ph)
Theorem	bnj1230 13773	First-order logic and set theory.
|- B = {x e. A | ph}   =>   |- (y e. B -> A.x y e. B)
Theorem	bnj1232 13774	First-order logic and set theory.
|- (ph <-> (ps /\ ch /\ th /\ ta))   =>   |- (ph -> ps)
Theorem	bnj1235 13775	First-order logic and set theory.
|- (ph <-> (ps /\ ch /\ th /\ ta))   =>   |- (ph -> ch)
Theorem	bnj1237 13776	First-order logic and set theory.
|- (E.x(ps /\ ch) -> E.xps)
Theorem	bnj1236 13777	First-order logic and set theory.
|- (ph <-> E.x(ps /\ ch))   =>   |- (ph -> E.xps)
Theorem	bnj1239 13778	First-order logic and set theory.
|- (E.x e. A (ps /\ ch) -> E.x e. A ps)
Theorem	bnj1238 13779	First-order logic and set theory.
|- (ph <-> E.x e. A (ps /\ ch))   =>   |- (ph -> E.x e. A ps)
Theorem	bnj1240 13780	First-order logic and set theory.
|- (ph -> A C_ B)   &   |- (ps -> A = C)   =>   |- ((ph /\ ps) -> C C_ B)
Theorem	bnj1241 13781	First-order logic and set theory.
|- (ph -> A C_ B)   &   |- (ps -> C = A)   =>   |- ((ph /\ ps) -> C C_ B)
Theorem	bnj1242 13782	First-order logic and set theory.
|- (ph -> A C_ B)   &   |- (ps -> A = C)   =>   |- ((ps /\ ph) -> C C_ B)
Theorem	bnj1243 13783	First-order logic and set theory.
|- (ph -> A C_ B)   &   |- (ps -> C = A)   =>   |- ((ps /\ ph) -> C C_ B)
Theorem	bnj1247 13784	First-order logic and set theory.
|- (ph <-> (ps /\ ch /\ th /\ ta))   =>   |- (ph -> th)
Theorem	bnj1249 13785	First-order logic and set theory.
|- (ph -> A C_ C)   =>   |- (ph -> (A i^i B) C_ C)
Theorem	bnj1250 13786	First-order logic and set theory.
|- (ph -> B C_ C)   =>   |- (ph -> (A i^i B) C_ C)
Theorem	bnj1251 13787	First-order logic and set theory.
|- A C_ B   &   |- (ph -> C C_ A)   =>   |- (ph -> C C_ B)
Theorem	bnj1252 13788	First-order logic and set theory.
|- A C_ B   &   |- (ph -> B C_ C)   =>   |- (ph -> A C_ C)
Theorem	bnj1254 13789	First-order logic and set theory.
|- (ph <-> (ps /\ ch /\ th /\ ta))   =>   |- (ph -> ta)
Theorem	bnj1260 13790	First-order logic and set theory.
|- ((ph /\ ps /\ ch) -> th)   &   |- ch   =>   |- ((ph /\ ps) -> th)
Theorem	bnj1261 13791	First-order logic and set theory.
|- A C_ B   &   |- (ph -> A = C)   =>   |- (ph -> C C_ B)
Theorem	bnj1262 13792	First-order logic and set theory.
|- A C_ B   &   |- (ph -> C = A)   =>   |- (ph -> C C_ B)
Theorem	bnj1264 13793	First-order logic and set theory.
|- B C_ A   &   |- (ph -> A = C)   =>   |- (ph -> B C_ C)
Theorem	bnj1263 13794	First-order logic and set theory.
|- B C_ A   &   |- (ph -> C = A)   =>   |- (ph -> B C_ C)
Theorem	bnj1266 13795	First-order logic and set theory.
|- (ch -> E.x(ph /\ ps))   =>   |- (ch -> E.xps)
Theorem	bnj1265 13796	First-order logic and set theory.
|- (ph -> E.x e. A ps)   =>   |- (ph -> ps)
Theorem	bnj1267 13797	First-order logic and set theory.
|- (ph <-> E.x(x e. A /\ ps))   =>   |- (ph <-> E.x e. A ps)
Theorem	bnj1269 13798	First-order logic and set theory.
|- ((A i^i B) =/= (/) <-> E.x(x e. A /\ x e. B))
Theorem	bnj1272 13799	First-order logic and set theory.
|- (ph -> A = B)   &   |- (ph -> C = D)   =>   |- (ph -> (A =/= C <-> B =/= D))
Theorem	bnj1273 13800	First-order logic and set theory.
|- (x = y -> (ph <-> ps))   &   |- (x = y -> (x e. A <-> y e. A))   =>   |- {x e. A | ph} = {y e. A | ps}