![]() |
Metamath
Proof Explorer Theorem List (p. 25 of 435) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-28329) |
![]() (28330-29854) |
![]() (29855-43446) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | nfeqf 2401 | A variable is effectively not free in an equality if it is not either of the involved variables. Ⅎ version of ax-c9 34964. (Contributed by Mario Carneiro, 6-Oct-2016.) Remove dependency on ax-11 2209. (Revised by Wolf Lammen, 6-Sep-2018.) |
⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦) → Ⅎ𝑧 𝑥 = 𝑦) | ||
Theorem | axc9 2402 | Derive set.mm's original ax-c9 34964 from the shorter ax-13 2390. (Contributed by NM, 29-Nov-2015.) (Revised by NM, 24-Dec-2015.) (Proof shortened by Wolf Lammen, 29-Apr-2018.) |
⊢ (¬ ∀𝑧 𝑧 = 𝑥 → (¬ ∀𝑧 𝑧 = 𝑦 → (𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦))) | ||
Theorem | ax6e 2403 |
At least one individual exists. This is not a theorem of free logic,
which is sound in empty domains. For such a logic, we would add this
theorem as an axiom of set theory (Axiom 0 of [Kunen] p. 10). In the
system consisting of ax-4 1910 through ax-9 2175,
all axioms other than
ax-6 2077 are believed to be theorems of free logic,
although the system
without ax-6 2077 is not complete in free logic.
It is preferred to use ax6ev 2079 when it is sufficient. (Contributed by NM, 14-May-1993.) Shortened after ax13lem1 2392 became available. (Revised by Wolf Lammen, 8-Sep-2018.) |
⊢ ∃𝑥 𝑥 = 𝑦 | ||
Theorem | ax6 2404 |
Theorem showing that ax-6 2077 follows from the weaker version ax6v 2078.
(Even though this theorem depends on ax-6 2077,
all references of ax-6 2077 are
made via ax6v 2078. An earlier version stated ax6v 2078
as a separate axiom,
but having two axioms caused some confusion.)
This theorem should be referenced in place of ax-6 2077 so that all proofs can be traced back to ax6v 2078. When possible, use the weaker ax6v 2078 rather than ax6 2404 since the ax6v 2078 derivation is much shorter and requires fewer axioms. (Contributed by NM, 12-Nov-2013.) (Revised by NM, 25-Jul-2015.) (Proof shortened by Wolf Lammen, 4-Feb-2018.) |
⊢ ¬ ∀𝑥 ¬ 𝑥 = 𝑦 | ||
Theorem | axc10 2405 |
Show that the original axiom ax-c10 34960 can be derived from ax6 2404
and axc7 2350
(on top of propositional calculus, ax-gen 1896, and ax-4 1910). See
ax6fromc10 34970 for the rederivation of ax6 2404
from ax-c10 34960.
Normally, axc10 2405 should be used rather than ax-c10 34960, except by theorems specifically studying the latter's properties. (Contributed by NM, 5-Aug-1993.) (Proof modification is discouraged.) |
⊢ (∀𝑥(𝑥 = 𝑦 → ∀𝑥𝜑) → 𝜑) | ||
Theorem | spimt 2406 | Closed theorem form of spim 2407. (Contributed by NM, 15-Jan-2008.) (Revised by Mario Carneiro, 17-Oct-2016.) (Proof shortened by Wolf Lammen, 24-Feb-2018.) |
⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝑦 → (𝜑 → 𝜓))) → (∀𝑥𝜑 → 𝜓)) | ||
Theorem | spim 2407 | Specialization, using implicit substitution. Compare Lemma 14 of [Tarski] p. 70. The spim 2407 series of theorems requires that only one direction of the substitution hypothesis hold. (Contributed by NM, 10-Jan-1993.) (Revised by Mario Carneiro, 3-Oct-2016.) (Proof shortened by Wolf Lammen, 18-Feb-2018.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) ⇒ ⊢ (∀𝑥𝜑 → 𝜓) | ||
Theorem | spimed 2408 | Deduction version of spime 2409. (Contributed by NM, 14-May-1993.) (Revised by Mario Carneiro, 3-Oct-2016.) (Proof shortened by Wolf Lammen, 19-Feb-2018.) |
⊢ (𝜒 → Ⅎ𝑥𝜑) & ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) ⇒ ⊢ (𝜒 → (𝜑 → ∃𝑥𝜓)) | ||
Theorem | spime 2409 | Existential introduction, using implicit substitution. Compare Lemma 14 of [Tarski] p. 70. (Contributed by NM, 7-Aug-1994.) (Revised by Mario Carneiro, 3-Oct-2016.) (Proof shortened by Wolf Lammen, 6-Mar-2018.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) ⇒ ⊢ (𝜑 → ∃𝑥𝜓) | ||
Theorem | spimv 2410* | A version of spim 2407 with a distinct variable requirement instead of a bound-variable hypothesis. See spimv1 2298 and spimvw 2105 for versions requiring fewer axioms. (Contributed by NM, 31-Jul-1993.) |
⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) ⇒ ⊢ (∀𝑥𝜑 → 𝜓) | ||
Theorem | spimvALT 2411* | Alternate proof of spimv 2410. Note that it requires only ax-1 6 through ax-5 2011 together with ax6e 2403. Currently, proofs derive from ax6v 2078, but if ax-6 2077 could be used instead, this proof would reduce axiom usage. (Contributed by NM, 31-Jul-1993.) Remove dependency on ax-10 2194. (Revised by BJ, 29-Nov-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) ⇒ ⊢ (∀𝑥𝜑 → 𝜓) | ||
Theorem | spimev 2412* | Distinct-variable version of spime 2409. (Contributed by NM, 10-Jan-1993.) |
⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) ⇒ ⊢ (𝜑 → ∃𝑥𝜓) | ||
Theorem | spv 2413* | Specialization, using implicit substitution. (Contributed by NM, 30-Aug-1993.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥𝜑 → 𝜓) | ||
Theorem | spei 2414 | Inference from existential specialization, using implicit substitution. Remove a distinct variable constraint. (Contributed by NM, 19-Aug-1993.) (Proof shortened by Wolf Lammen, 12-May-2018.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ 𝜓 ⇒ ⊢ ∃𝑥𝜑 | ||
Theorem | chvar 2415 | Implicit substitution of 𝑦 for 𝑥 into a theorem. (Contributed by Raph Levien, 9-Jul-2003.) (Revised by Mario Carneiro, 3-Oct-2016.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ 𝜑 ⇒ ⊢ 𝜓 | ||
Theorem | chvarv 2416* | Implicit substitution of 𝑦 for 𝑥 into a theorem. (Contributed by NM, 20-Apr-1994.) (Proof shortened by Wolf Lammen, 22-Apr-2018.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ 𝜑 ⇒ ⊢ 𝜓 | ||
Theorem | cbv3 2417 | Rule used to change bound variables, using implicit substitution, that does not use ax-c9 34964. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 12-May-2018.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) ⇒ ⊢ (∀𝑥𝜑 → ∀𝑦𝜓) | ||
Theorem | cbv3h 2418 | Rule used to change bound variables, using implicit substitution. (Contributed by NM, 8-Jun-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 12-May-2018.) |
⊢ (𝜑 → ∀𝑦𝜑) & ⊢ (𝜓 → ∀𝑥𝜓) & ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) ⇒ ⊢ (∀𝑥𝜑 → ∀𝑦𝜓) | ||
Theorem | cbv1 2419 | Rule used to change bound variables, using implicit substitution. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 3-Oct-2016.) Format hypotheses to common style. (Revised by Wolf Lammen, 13-May-2018.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑦𝜓) & ⊢ (𝜑 → Ⅎ𝑥𝜒) & ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 → 𝜒))) ⇒ ⊢ (𝜑 → (∀𝑥𝜓 → ∀𝑦𝜒)) | ||
Theorem | cbv1h 2420 | Rule used to change bound variables, using implicit substitution. (Contributed by NM, 11-May-1993.) (Proof shortened by Wolf Lammen, 13-May-2018.) |
⊢ (𝜑 → (𝜓 → ∀𝑦𝜓)) & ⊢ (𝜑 → (𝜒 → ∀𝑥𝜒)) & ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 → 𝜒))) ⇒ ⊢ (∀𝑥∀𝑦𝜑 → (∀𝑥𝜓 → ∀𝑦𝜒)) | ||
Theorem | cbv2h 2421 | Rule used to change bound variables, using implicit substitution. (Contributed by NM, 11-May-1993.) |
⊢ (𝜑 → (𝜓 → ∀𝑦𝜓)) & ⊢ (𝜑 → (𝜒 → ∀𝑥𝜒)) & ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))) ⇒ ⊢ (∀𝑥∀𝑦𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒)) | ||
Theorem | cbv2 2422 | Rule used to change bound variables, using implicit substitution. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 3-Oct-2016.) Format hypotheses to common style. (Revised by Wolf Lammen, 13-May-2018.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑦𝜓) & ⊢ (𝜑 → Ⅎ𝑥𝜒) & ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))) ⇒ ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒)) | ||
Theorem | cbval 2423 | Rule used to change bound variables, using implicit substitution. (Contributed by NM, 13-May-1993.) (Revised by Mario Carneiro, 3-Oct-2016.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓) | ||
Theorem | cbvex 2424 | Rule used to change bound variables, using implicit substitution. (Contributed by NM, 21-Jun-1993.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓) | ||
Theorem | cbvalv 2425* | Rule used to change bound variables, using implicit substitution. See cbvalvw 2145 for a version requiring fewer axioms, to be preferred when sufficient. (Contributed by NM, 5-Aug-1993.) Remove dependency on ax-10 2194. (Revised by Wolf Lammen, 17-Jul-2021.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓) | ||
Theorem | cbvexv 2426* | Rule used to change bound variables, using implicit substitution. See cbvexvw 2146 for a version requiring fewer axioms, to be preferred when sufficient. (Contributed by NM, 21-Jun-1993.) Remove dependency on ax-10 2194. (Revised by Wolf Lammen, 17-Jul-2021.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓) | ||
Theorem | cbvald 2427* | Deduction used to change bound variables, using implicit substitution, particularly useful in conjunction with dvelim 2471. (Contributed by NM, 2-Jan-2002.) (Revised by Mario Carneiro, 6-Oct-2016.) (Revised by Wolf Lammen, 13-May-2018.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑦𝜓) & ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))) ⇒ ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒)) | ||
Theorem | cbvexd 2428* | Deduction used to change bound variables, using implicit substitution, particularly useful in conjunction with dvelim 2471. (Contributed by NM, 2-Jan-2002.) (Revised by Mario Carneiro, 6-Oct-2016.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑦𝜓) & ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))) ⇒ ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑦𝜒)) | ||
Theorem | cbval2 2429* | Rule used to change bound variables, using implicit substitution. (Contributed by NM, 22-Dec-2003.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof shortened by Wolf Lammen, 22-Apr-2018.) |
⊢ Ⅎ𝑧𝜑 & ⊢ Ⅎ𝑤𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ Ⅎ𝑦𝜓 & ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑧∀𝑤𝜓) | ||
Theorem | cbvex2 2430* | Rule used to change bound variables, using implicit substitution. (Contributed by NM, 14-Sep-2003.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof shortened by Wolf Lammen, 16-Jun-2019.) |
⊢ Ⅎ𝑧𝜑 & ⊢ Ⅎ𝑤𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ Ⅎ𝑦𝜓 & ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑧∃𝑤𝜓) | ||
Theorem | cbvaldva 2431* | Rule used to change the bound variable in a universal quantifier with implicit substitution. Deduction form. (Contributed by David Moews, 1-May-2017.) Remove dependency on ax-10 2194. (Revised by Wolf Lammen, 18-Jul-2021.) |
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒)) | ||
Theorem | cbvexdva 2432* | Rule used to change the bound variable in an existential quantifier with implicit substitution. Deduction form. (Contributed by David Moews, 1-May-2017.) Remove dependency on ax-10 2194. (Revised by Wolf Lammen, 18-Jul-2021.) |
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑦𝜒)) | ||
Theorem | cbval2v 2433* | Rule used to change bound variables, using implicit substitution. (Contributed by NM, 4-Feb-2005.) Remove dependency on ax-10 2194. (Revised by Wolf Lammen, 18-Jul-2021.) |
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑧∀𝑤𝜓) | ||
Theorem | cbvex2v 2434* | Rule used to change bound variables, using implicit substitution. (Contributed by NM, 26-Jul-1995.) Remove dependency on ax-10 2194. (Revised by Wolf Lammen, 18-Jul-2021.) |
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑧∃𝑤𝜓) | ||
Theorem | cbvex4v 2435* | Rule used to change bound variables, using implicit substitution. (Contributed by NM, 26-Jul-1995.) |
⊢ ((𝑥 = 𝑣 ∧ 𝑦 = 𝑢) → (𝜑 ↔ 𝜓)) & ⊢ ((𝑧 = 𝑓 ∧ 𝑤 = 𝑔) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (∃𝑥∃𝑦∃𝑧∃𝑤𝜑 ↔ ∃𝑣∃𝑢∃𝑓∃𝑔𝜒) | ||
Theorem | equs4 2436 | Lemma used in proofs of implicit substitution properties. The converse requires either a disjoint variable condition (sb56 2307) or a non-freeness hypothesis (equs45f 2479). See equs4v 2109 for a version requiring fewer axioms. (Contributed by NM, 10-May-1993.) (Proof shortened by Mario Carneiro, 20-May-2014.) (Proof shortened by Wolf Lammen, 5-Feb-2018.) |
⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) | ||
Theorem | equsal 2437 | An equivalence related to implicit substitution. See equsalvw 2110 and equsalv 2300 for versions with disjoint variable conditions proved from fewer axioms. See also the dual form equsex 2438. (Contributed by NM, 2-Jun-1993.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) (Revised by Mario Carneiro, 3-Oct-2016.) (Proof shortened by Wolf Lammen, 5-Feb-2018.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓) | ||
Theorem | equsex 2438 | An equivalence related to implicit substitution. See equsexvw 2111 and equsexv 2301 for versions with disjoint variable conditions proved from fewer axioms. See also the dual form equsal 2437. See equsexALT 2439 for an alternate proof. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 3-Oct-2016.) (Proof shortened by Wolf Lammen, 6-Feb-2018.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ 𝜓) | ||
Theorem | equsexALT 2439 | Alternate proof of equsex 2438. This proves the result directly, instead of as a corollary of equsal 2437 via equs4 2436. Note in particular that only existential quantifiers appear in the proof and that the only step requiring ax-13 2390 is ax6e 2403. This proof mimics that of equsal 2437 (in particular, note that pm5.32i 572, exbii 1949, 19.41 2280, mpbiran 702 correspond respectively to pm5.74i 263, albii 1920, 19.23 2256, a1bi 354). (Contributed by BJ, 20-Aug-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ 𝜓) | ||
Theorem | equsalh 2440 | An equivalence related to implicit substitution. See equsalhw 2324 for a version with a disjoint variable condition requiring fewer axioms. (Contributed by NM, 2-Jun-1993.) |
⊢ (𝜓 → ∀𝑥𝜓) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓) | ||
Theorem | equsexh 2441 | An equivalence related to implicit substitution. See equsexhv 2326 for a version with a disjoint variable condition which does not require ax-13 2390. (Contributed by NM, 5-Aug-1993.) |
⊢ (𝜓 → ∀𝑥𝜓) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ 𝜓) | ||
Theorem | axc15 2442 |
Derivation of set.mm's original ax-c15 34963 from ax-c11n 34962 and the shorter
ax-12 2222 that has replaced it.
Theorem ax12 2443 shows the reverse derivation of ax-12 2222 from ax-c15 34963. Normally, axc15 2442 should be used rather than ax-c15 34963, except by theorems specifically studying the latter's properties. (Contributed by NM, 2-Feb-2007.) (Proof shortened by Wolf Lammen, 21-Apr-2018.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))) | ||
Theorem | ax12 2443 | Rederivation of axiom ax-12 2222 from ax12v 2223 (used only via sp 2226) , axc11r 2389, and axc15 2442 (on top of Tarski's FOL). (Contributed by NM, 22-Jan-2007.) Proof uses contemporary axioms. (Revised by Wolf Lammen, 8-Aug-2020.) (Proof shortened by BJ, 4-Jul-2021.) |
⊢ (𝑥 = 𝑦 → (∀𝑦𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) | ||
Theorem | ax12b 2444 | A bidirectional version of axc15 2442. (Contributed by NM, 30-Jun-2006.) |
⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦) → (𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑))) | ||
Theorem | ax13ALT 2445 | Alternate proof of ax13 2393 from FOL, sp 2226, and axc9 2402. (Contributed by NM, 21-Dec-2015.) (Proof shortened by Wolf Lammen, 31-Jan-2018.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ 𝑥 = 𝑦 → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧)) | ||
Theorem | axc11n 2446 | Derive set.mm's original ax-c11n 34962 from others. Commutation law for identical variable specifiers. The antecedent and consequent are true when 𝑥 and 𝑦 are substituted with the same variable. Lemma L12 in [Megill] p. 445 (p. 12 of the preprint). If a disjoint variable condition is added on 𝑥 and 𝑦, then this becomes an instance of aevlem 2157. Use aecom 2447 instead when this does not lengthen the proof. (Contributed by NM, 10-May-1993.) (Revised by NM, 7-Nov-2015.) (Proof shortened by Wolf Lammen, 6-Mar-2018.) (Revised by Wolf Lammen, 30-Nov-2019.) (Proof shortened by BJ, 29-Mar-2021.) (Proof shortened by Wolf Lammen, 2-Jul-2021.) |
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥) | ||
Theorem | aecom 2447 | Commutation law for identical variable specifiers. Both sides of the biconditional are true when 𝑥 and 𝑦 are substituted with the same variable. (Contributed by NM, 10-May-1993.) Change to a biconditional. (Revised by BJ, 26-Sep-2019.) |
⊢ (∀𝑥 𝑥 = 𝑦 ↔ ∀𝑦 𝑦 = 𝑥) | ||
Theorem | aecoms 2448 | A commutation rule for identical variable specifiers. (Contributed by NM, 10-May-1993.) |
⊢ (∀𝑥 𝑥 = 𝑦 → 𝜑) ⇒ ⊢ (∀𝑦 𝑦 = 𝑥 → 𝜑) | ||
Theorem | naecoms 2449 | A commutation rule for distinct variable specifiers. (Contributed by NM, 2-Jan-2002.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → 𝜑) ⇒ ⊢ (¬ ∀𝑦 𝑦 = 𝑥 → 𝜑) | ||
Theorem | axc11 2450 | Show that ax-c11 34961 can be derived from ax-c11n 34962 in the form of axc11n 2446. Normally, axc11 2450 should be used rather than ax-c11 34961, except by theorems specifically studying the latter's properties. (Contributed by NM, 16-May-2008.) (Proof shortened by Wolf Lammen, 21-Apr-2018.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 → ∀𝑦𝜑)) | ||
Theorem | hbae 2451 | All variables are effectively bound in an identical variable specifier. (Contributed by NM, 13-May-1993.) (Proof shortened by Wolf Lammen, 21-Apr-2018.) |
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧∀𝑥 𝑥 = 𝑦) | ||
Theorem | nfae 2452 | All variables are effectively bound in an identical variable specifier. (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ Ⅎ𝑧∀𝑥 𝑥 = 𝑦 | ||
Theorem | hbnae 2453 | All variables are effectively bound in a distinct variable specifier. A version with a distinct variable condition based on fewer axioms is hbnaev 2163. Lemma L19 in [Megill] p. 446 (p. 14 of the preprint). (Contributed by NM, 13-May-1993.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑧 ¬ ∀𝑥 𝑥 = 𝑦) | ||
Theorem | nfnae 2454 | All variables are effectively bound in a distinct variable specifier. (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ Ⅎ𝑧 ¬ ∀𝑥 𝑥 = 𝑦 | ||
Theorem | hbnaes 2455 | Rule that applies hbnae 2453 to antecedent. (Contributed by NM, 15-May-1993.) |
⊢ (∀𝑧 ¬ ∀𝑥 𝑥 = 𝑦 → 𝜑) ⇒ ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → 𝜑) | ||
Theorem | axc16i 2456* | Inference with axc16 2293 as its conclusion. (Contributed by NM, 20-May-2008.) (Proof modification is discouraged.) |
⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜓)) & ⊢ (𝜓 → ∀𝑥𝜓) ⇒ ⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑥𝜑)) | ||
Theorem | axc16nfALT 2457* | Alternate proof of axc16nf 2295, shorter but requiring ax-11 2209 and ax-13 2390. (Contributed by Mario Carneiro, 7-Oct-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → Ⅎ𝑧𝜑) | ||
Theorem | dral2 2458 | Formula-building lemma for use with the Distinctor Reduction Theorem. Part of Theorem 9.4 of [Megill] p. 448 (p. 16 of preprint). (Contributed by NM, 27-Feb-2005.) Allow a shortening of dral1 2459. (Revised by Wolf Lammen, 4-Mar-2018.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑧𝜑 ↔ ∀𝑧𝜓)) | ||
Theorem | dral1 2459 | Formula-building lemma for use with the Distinctor Reduction Theorem. Part of Theorem 9.4 of [Megill] p. 448 (p. 16 of preprint). (Contributed by NM, 24-Nov-1994.) Remove dependency on ax-11 2209. (Revised by Wolf Lammen, 6-Sep-2018.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 ↔ ∀𝑦𝜓)) | ||
Theorem | dral1ALT 2460 | Alternate proof of dral1 2459, shorter but requiring ax-11 2209. (Contributed by NM, 24-Nov-1994.) (Proof shortened by Wolf Lammen, 22-Apr-2018.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 ↔ ∀𝑦𝜓)) | ||
Theorem | drex1 2461 | Formula-building lemma for use with the Distinctor Reduction Theorem. Part of Theorem 9.4 of [Megill] p. 448 (p. 16 of preprint). (Contributed by NM, 27-Feb-2005.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 𝑥 = 𝑦 → (∃𝑥𝜑 ↔ ∃𝑦𝜓)) | ||
Theorem | drex2 2462 | Formula-building lemma for use with the Distinctor Reduction Theorem. Part of Theorem 9.4 of [Megill] p. 448 (p. 16 of preprint). (Contributed by NM, 27-Feb-2005.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 𝑥 = 𝑦 → (∃𝑧𝜑 ↔ ∃𝑧𝜓)) | ||
Theorem | drnf1 2463 | Formula-building lemma for use with the Distinctor Reduction Theorem. (Contributed by Mario Carneiro, 4-Oct-2016.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 𝑥 = 𝑦 → (Ⅎ𝑥𝜑 ↔ Ⅎ𝑦𝜓)) | ||
Theorem | drnf2 2464 | Formula-building lemma for use with the Distinctor Reduction Theorem. (Contributed by Mario Carneiro, 4-Oct-2016.) (Proof shortened by Wolf Lammen, 5-May-2018.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 𝑥 = 𝑦 → (Ⅎ𝑧𝜑 ↔ Ⅎ𝑧𝜓)) | ||
Theorem | nfald2 2465 | Variation on nfald 2362 which adds the hypothesis that 𝑥 and 𝑦 are distinct in the inner subproof. (Contributed by Mario Carneiro, 8-Oct-2016.) |
⊢ Ⅎ𝑦𝜑 & ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥𝜓) ⇒ ⊢ (𝜑 → Ⅎ𝑥∀𝑦𝜓) | ||
Theorem | nfexd2 2466 | Variation on nfexd 2363 which adds the hypothesis that 𝑥 and 𝑦 are distinct in the inner subproof. (Contributed by Mario Carneiro, 8-Oct-2016.) |
⊢ Ⅎ𝑦𝜑 & ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥𝜓) ⇒ ⊢ (𝜑 → Ⅎ𝑥∃𝑦𝜓) | ||
Theorem | exdistrf 2467 | Distribution of existential quantifiers, with a bound-variable hypothesis saying that 𝑦 is not free in 𝜑, but 𝑥 can be free in 𝜑 (and there is no distinct variable condition on 𝑥 and 𝑦). (Contributed by Mario Carneiro, 20-Mar-2013.) (Proof shortened by Wolf Lammen, 14-May-2018.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦𝜑) ⇒ ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) → ∃𝑥(𝜑 ∧ ∃𝑦𝜓)) | ||
Theorem | dvelimf 2468 | Version of dvelimv 2472 without any variable restrictions. (Contributed by NM, 1-Oct-2002.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof shortened by Wolf Lammen, 11-May-2018.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑧𝜓 & ⊢ (𝑧 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝜓) | ||
Theorem | dvelimdf 2469 | Deduction form of dvelimf 2468. (Contributed by NM, 7-Apr-2004.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof shortened by Wolf Lammen, 11-May-2018.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑧𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝜓) & ⊢ (𝜑 → Ⅎ𝑧𝜒) & ⊢ (𝜑 → (𝑧 = 𝑦 → (𝜓 ↔ 𝜒))) ⇒ ⊢ (𝜑 → (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝜒)) | ||
Theorem | dvelimh 2470 | Version of dvelim 2471 without any variable restrictions. (Contributed by NM, 1-Oct-2002.) (Proof shortened by Wolf Lammen, 11-May-2018.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜓 → ∀𝑧𝜓) & ⊢ (𝑧 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝜓 → ∀𝑥𝜓)) | ||
Theorem | dvelim 2471* |
This theorem can be used to eliminate a distinct variable restriction on
𝑥 and 𝑧 and replace it with the
"distinctor" ¬ ∀𝑥𝑥 = 𝑦
as an antecedent. 𝜑 normally has 𝑧 free and can be read
𝜑(𝑧), and 𝜓 substitutes 𝑦 for
𝑧
and can be read
𝜑(𝑦). We do not require that 𝑥 and
𝑦
be distinct: if
they are not, the distinctor will become false (in multiple-element
domains of discourse) and "protect" the consequent.
To obtain a closed-theorem form of this inference, prefix the hypotheses with ∀𝑥∀𝑧, conjoin them, and apply dvelimdf 2469. Other variants of this theorem are dvelimh 2470 (with no distinct variable restrictions) and dvelimhw 2371 (that avoids ax-13 2390). (Contributed by NM, 23-Nov-1994.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝑧 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝜓 → ∀𝑥𝜓)) | ||
Theorem | dvelimv 2472* | Similar to dvelim 2471 with first hypothesis replaced by a distinct variable condition. (Contributed by NM, 25-Jul-2015.) (Proof shortened by Wolf Lammen, 30-Apr-2018.) |
⊢ (𝑧 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝜓 → ∀𝑥𝜓)) | ||
Theorem | dvelimnf 2473* | Version of dvelim 2471 using "not free" notation. (Contributed by Mario Carneiro, 9-Oct-2016.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝑧 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝜓) | ||
Theorem | dveeq2ALT 2474* | Alternate proof of dveeq2 2398, shorter but requiring ax-11 2209. (Contributed by NM, 2-Jan-2002.) (Revised by NM, 20-Jul-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦)) | ||
Theorem | equvini 2475 | A variable introduction law for equality. Lemma 15 of [Monk2] p. 109, however we do not require 𝑧 to be distinct from 𝑥 and 𝑦. See equvinv 2136 for a shorter proof requiring fewer axioms when 𝑧 is required to be distinct from 𝑥 and 𝑦. (Contributed by NM, 10-Jan-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 15-Sep-2018.) |
⊢ (𝑥 = 𝑦 → ∃𝑧(𝑥 = 𝑧 ∧ 𝑧 = 𝑦)) | ||
Theorem | equvel 2476 | A variable elimination law for equality with no distinct variable requirements. Compare equvini 2475. (Contributed by NM, 1-Mar-2013.) (Proof shortened by Mario Carneiro, 17-Oct-2016.) (Proof shortened by Wolf Lammen, 15-Jun-2019.) |
⊢ (∀𝑧(𝑧 = 𝑥 ↔ 𝑧 = 𝑦) → 𝑥 = 𝑦) | ||
Theorem | equs5a 2477 | A property related to substitution that unlike equs5 2480 does not require a distinctor antecedent. See equs5aALT 2387 for an alternate proof using ax-12 2222 but not ax13 2393. (Contributed by NM, 2-Feb-2007.) |
⊢ (∃𝑥(𝑥 = 𝑦 ∧ ∀𝑦𝜑) → ∀𝑥(𝑥 = 𝑦 → 𝜑)) | ||
Theorem | equs5e 2478 | A property related to substitution that unlike equs5 2480 does not require a distinctor antecedent. See equs5eALT 2388 for an alternate proof using ax-12 2222 but not ax13 2393. (Contributed by NM, 2-Feb-2007.) (Proof shortened by Wolf Lammen, 15-Jan-2018.) |
⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑦 → ∃𝑦𝜑)) | ||
Theorem | equs45f 2479 | Two ways of expressing substitution when 𝑦 is not free in 𝜑. The implication "to the left" is equs4 2436 and does not require the non-freeness hypothesis. Theorem sb56 2307 replaces the non-freeness hypothesis with a disjoint variable condition and equs5 2480 replaces it with a distinctor as antecedent. (Contributed by NM, 25-Apr-2008.) (Revised by Mario Carneiro, 4-Oct-2016.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑)) | ||
Theorem | equs5 2480 | Lemma used in proofs of substitution properties. If there is a disjoint variable condition on 𝑥, 𝑦, then sb56 2307 can be used instead; if 𝑦 is not free in 𝜑, then equs45f 2479 can be used. (Contributed by NM, 14-May-1993.) (Revised by BJ, 1-Oct-2018.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑))) | ||
Theorem | sb2 2481 | One direction of a simplified definition of substitution. The converse requires either a disjoint variable condition (sb6 2309) or a non-freeness hypothesis (sb6f 2515). (Contributed by NM, 13-May-1993.) |
⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → [𝑦 / 𝑥]𝜑) | ||
Theorem | stdpc4 2482 | The specialization axiom of standard predicate calculus. It states that if a statement 𝜑 holds for all 𝑥, then it also holds for the specific case of 𝑦 (properly) substituted for 𝑥. Translated to traditional notation, it can be read: "∀𝑥𝜑(𝑥) → 𝜑(𝑦), provided that 𝑦 is free for 𝑥 in 𝜑(𝑥)". Axiom 4 of [Mendelson] p. 69. See also spsbc 3674 and rspsbc 3741. For a version requiring disjoint variables, but fewer axioms, see stdpc4v 2303. (Contributed by NM, 14-May-1993.) |
⊢ (∀𝑥𝜑 → [𝑦 / 𝑥]𝜑) | ||
Theorem | 2stdpc4 2483 | A double specialization using explicit substitution. This is Theorem PM*11.1 in [WhiteheadRussell] p. 159. See stdpc4 2482 for the analogous single specialization. See 2sp 2229 for another double specialization. (Contributed by Andrew Salmon, 24-May-2011.) (Revised by BJ, 21-Oct-2018.) |
⊢ (∀𝑥∀𝑦𝜑 → [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) | ||
Theorem | sb3 2484 | One direction of a simplified definition of substitution when variables are distinct. (Contributed by NM, 5-Aug-1993.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → [𝑦 / 𝑥]𝜑)) | ||
Theorem | sb3b 2485 | Simplified definition of substitution when variables are distinct. This is to sb3 2484 what sb4b 2488 is to sb4 2486. (Contributed by BJ, 6-Oct-2018.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) | ||
Theorem | sb4 2486 | One direction of a simplified definition of substitution when variables are distinct. (Contributed by NM, 14-May-1993.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ([𝑦 / 𝑥]𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) | ||
Theorem | sb4a 2487 | A version of sb4 2486 that does not require a distinctor antecedent. (Contributed by NM, 2-Feb-2007.) |
⊢ ([𝑦 / 𝑥]∀𝑦𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)) | ||
Theorem | sb4b 2488 | Simplified definition of substitution when variables are distinct. (Contributed by NM, 27-May-1997.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ([𝑦 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑))) | ||
Theorem | hbsb2 2489 | Bound-variable hypothesis builder for substitution. (Contributed by NM, 14-May-1993.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑)) | ||
Theorem | nfsb2 2490 | Bound-variable hypothesis builder for substitution. (Contributed by Mario Carneiro, 4-Oct-2016.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥[𝑦 / 𝑥]𝜑) | ||
Theorem | hbsb2a 2491 | Special case of a bound-variable hypothesis builder for substitution. (Contributed by NM, 2-Feb-2007.) |
⊢ ([𝑦 / 𝑥]∀𝑦𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑) | ||
Theorem | sb4e 2492 | One direction of a simplified definition of substitution that unlike sb4 2486 does not require a distinctor antecedent. (Contributed by NM, 2-Feb-2007.) |
⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥(𝑥 = 𝑦 → ∃𝑦𝜑)) | ||
Theorem | hbsb2e 2493 | Special case of a bound-variable hypothesis builder for substitution. (Contributed by NM, 2-Feb-2007.) |
⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]∃𝑦𝜑) | ||
Theorem | hbsb3 2494 | If 𝑦 is not free in 𝜑, 𝑥 is not free in [𝑦 / 𝑥]𝜑. (Contributed by NM, 14-May-1993.) |
⊢ (𝜑 → ∀𝑦𝜑) ⇒ ⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑) | ||
Theorem | nfs1 2495 | If 𝑦 is not free in 𝜑, 𝑥 is not free in [𝑦 / 𝑥]𝜑. (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑 | ||
Theorem | axc16ALT 2496* | Alternate proof of axc16 2293, shorter but requiring ax-10 2194, ax-11 2209, ax-13 2390 and using df-nf 1885 and df-sb 2070. (Contributed by NM, 17-May-2008.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑥𝜑)) | ||
Theorem | axc16gALT 2497* | Alternate proof of axc16g 2292 that uses df-sb 2070 and requires ax-10 2194, ax-11 2209, ax-13 2390. (Contributed by NM, 15-May-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑧𝜑)) | ||
Theorem | equsb1 2498 | Substitution applied to an atomic wff. (Contributed by NM, 10-May-1993.) |
⊢ [𝑦 / 𝑥]𝑥 = 𝑦 | ||
Theorem | equsb2 2499 | Substitution applied to an atomic wff. (Contributed by NM, 10-May-1993.) |
⊢ [𝑦 / 𝑥]𝑦 = 𝑥 | ||
Theorem | dveel1 2500* | Quantifier introduction when one pair of variables is distinct. (Contributed by NM, 2-Jan-2002.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦 ∈ 𝑧 → ∀𝑥 𝑦 ∈ 𝑧)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |