![]() |
Intuitionistic Logic Explorer Theorem List (p. 28 of 150) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cbvral 2701* | Rule used to change bound variables, using implicit substitution. (Contributed by NM, 31-Jul-2003.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓) | ||
Theorem | cbvrex 2702* | Rule used to change bound variables, using implicit substitution. (Contributed by NM, 31-Jul-2003.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓) | ||
Theorem | cbvreu 2703* | Change the bound variable of a restricted unique existential quantifier using implicit substitution. (Contributed by Mario Carneiro, 15-Oct-2016.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑦 ∈ 𝐴 𝜓) | ||
Theorem | cbvrmo 2704* | Change the bound variable of restricted "at most one" using implicit substitution. (Contributed by NM, 16-Jun-2017.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑦 ∈ 𝐴 𝜓) | ||
Theorem | cbvralv 2705* | Change the bound variable of a restricted universal quantifier using implicit substitution. (Contributed by NM, 28-Jan-1997.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓) | ||
Theorem | cbvrexv 2706* | Change the bound variable of a restricted existential quantifier using implicit substitution. (Contributed by NM, 2-Jun-1998.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓) | ||
Theorem | cbvreuv 2707* | Change the bound variable of a restricted unique existential quantifier using implicit substitution. (Contributed by NM, 5-Apr-2004.) (Revised by Mario Carneiro, 15-Oct-2016.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑦 ∈ 𝐴 𝜓) | ||
Theorem | cbvrmov 2708* | Change the bound variable of a restricted at-most-one quantifier using implicit substitution. (Contributed by Alexander van der Vekens, 17-Jun-2017.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑦 ∈ 𝐴 𝜓) | ||
Theorem | cbvralvw 2709* | Version of cbvralv 2705 with a disjoint variable condition. (Contributed by Gino Giotto, 10-Jan-2024.) Reduce axiom usage. (Revised by Gino Giotto, 25-Aug-2024.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓) | ||
Theorem | cbvrexvw 2710* | Version of cbvrexv 2706 with a disjoint variable condition. (Contributed by Gino Giotto, 10-Jan-2024.) Reduce axiom usage. (Revised by Gino Giotto, 25-Aug-2024.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓) | ||
Theorem | cbvreuvw 2711* | Version of cbvreuv 2707 with a disjoint variable condition. (Contributed by Gino Giotto, 10-Jan-2024.) Reduce axiom usage. (Revised by Gino Giotto, 25-Aug-2024.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑦 ∈ 𝐴 𝜓) | ||
Theorem | cbvraldva2 2712* | Rule used to change the bound variable in a restricted universal quantifier with implicit substitution which also changes the quantifier domain. Deduction form. (Contributed by David Moews, 1-May-2017.) |
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) & ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑦 ∈ 𝐵 𝜒)) | ||
Theorem | cbvrexdva2 2713* | Rule used to change the bound variable in a restricted existential quantifier with implicit substitution which also changes the quantifier domain. Deduction form. (Contributed by David Moews, 1-May-2017.) |
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) & ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑦 ∈ 𝐵 𝜒)) | ||
Theorem | cbvraldva 2714* | Rule used to change the bound variable in a restricted universal quantifier with implicit substitution. Deduction form. (Contributed by David Moews, 1-May-2017.) |
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑦 ∈ 𝐴 𝜒)) | ||
Theorem | cbvrexdva 2715* | Rule used to change the bound variable in a restricted existential quantifier with implicit substitution. Deduction form. (Contributed by David Moews, 1-May-2017.) |
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑦 ∈ 𝐴 𝜒)) | ||
Theorem | cbvral2vw 2716* | Change bound variables of double restricted universal quantification, using implicit substitution. Version of cbvral2v 2718 with a disjoint variable condition, which does not require ax-13 2150. (Contributed by NM, 10-Aug-2004.) (Revised by Gino Giotto, 10-Jan-2024.) |
⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜒)) & ⊢ (𝑦 = 𝑤 → (𝜒 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐵 𝜓) | ||
Theorem | cbvrex2vw 2717* | Change bound variables of double restricted universal quantification, using implicit substitution. Version of cbvrex2v 2719 with a disjoint variable condition, which does not require ax-13 2150. (Contributed by FL, 2-Jul-2012.) (Revised by Gino Giotto, 10-Jan-2024.) |
⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜒)) & ⊢ (𝑦 = 𝑤 → (𝜒 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝜓) | ||
Theorem | cbvral2v 2718* | Change bound variables of double restricted universal quantification, using implicit substitution. (Contributed by NM, 10-Aug-2004.) |
⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜒)) & ⊢ (𝑦 = 𝑤 → (𝜒 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐵 𝜓) | ||
Theorem | cbvrex2v 2719* | Change bound variables of double restricted universal quantification, using implicit substitution. (Contributed by FL, 2-Jul-2012.) |
⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜒)) & ⊢ (𝑦 = 𝑤 → (𝜒 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝜓) | ||
Theorem | cbvral3v 2720* | Change bound variables of triple restricted universal quantification, using implicit substitution. (Contributed by NM, 10-May-2005.) |
⊢ (𝑥 = 𝑤 → (𝜑 ↔ 𝜒)) & ⊢ (𝑦 = 𝑣 → (𝜒 ↔ 𝜃)) & ⊢ (𝑧 = 𝑢 → (𝜃 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜑 ↔ ∀𝑤 ∈ 𝐴 ∀𝑣 ∈ 𝐵 ∀𝑢 ∈ 𝐶 𝜓) | ||
Theorem | cbvralsv 2721* | Change bound variable by using a substitution. (Contributed by NM, 20-Nov-2005.) (Revised by Andrew Salmon, 11-Jul-2011.) |
⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 [𝑦 / 𝑥]𝜑) | ||
Theorem | cbvrexsv 2722* | Change bound variable by using a substitution. (Contributed by NM, 2-Mar-2008.) (Revised by Andrew Salmon, 11-Jul-2011.) |
⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 [𝑦 / 𝑥]𝜑) | ||
Theorem | sbralie 2723* | Implicit to explicit substitution that swaps variables in a quantified expression. (Contributed by NM, 5-Sep-2004.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝑦 𝜑 ↔ [𝑦 / 𝑥]∀𝑦 ∈ 𝑥 𝜓) | ||
Theorem | rabbiia 2724 | Equivalent wff's yield equal restricted class abstractions (inference form). (Contributed by NM, 22-May-1999.) |
⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐴 ∣ 𝜓} | ||
Theorem | rabbii 2725 | Equivalent wff's correspond to equal restricted class abstractions. Inference form of rabbidv 2728. (Contributed by Peter Mazsa, 1-Nov-2019.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐴 ∣ 𝜓} | ||
Theorem | rabbidva2 2726* | Equivalent wff's yield equal restricted class abstractions. (Contributed by Thierry Arnoux, 4-Feb-2017.) |
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐵 ∧ 𝜒))) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒}) | ||
Theorem | rabbidva 2727* | Equivalent wff's yield equal restricted class abstractions (deduction form). (Contributed by NM, 28-Nov-2003.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒}) | ||
Theorem | rabbidv 2728* | Equivalent wff's yield equal restricted class abstractions (deduction form). (Contributed by NM, 10-Feb-1995.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒}) | ||
Theorem | rabeqf 2729 | Equality theorem for restricted class abstractions, with bound-variable hypotheses instead of distinct variable restrictions. (Contributed by NM, 7-Mar-2004.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜑}) | ||
Theorem | rabeqif 2730 | Equality theorem for restricted class abstractions. Inference form of rabeqf 2729. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ 𝐴 = 𝐵 ⇒ ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜑} | ||
Theorem | rabeq 2731* | Equality theorem for restricted class abstractions. (Contributed by NM, 15-Oct-2003.) |
⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜑}) | ||
Theorem | rabeqi 2732* | Equality theorem for restricted class abstractions. Inference form of rabeq 2731. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜑} | ||
Theorem | rabeqdv 2733* | Equality of restricted class abstractions. Deduction form of rabeq 2731. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜓}) | ||
Theorem | rabeqbidv 2734* | Equality of restricted class abstractions. (Contributed by Jeff Madsen, 1-Dec-2009.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒}) | ||
Theorem | rabeqbidva 2735* | Equality of restricted class abstractions. (Contributed by Mario Carneiro, 26-Jan-2017.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒}) | ||
Theorem | rabeq2i 2736 | Inference from equality of a class variable and a restricted class abstraction. (Contributed by NM, 16-Feb-2004.) |
⊢ 𝐴 = {𝑥 ∈ 𝐵 ∣ 𝜑} ⇒ ⊢ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐵 ∧ 𝜑)) | ||
Theorem | cbvrab 2737 | Rule to change the bound variable in a restricted class abstraction, using implicit substitution. This version has bound-variable hypotheses in place of distinct variable conditions. (Contributed by Andrew Salmon, 11-Jul-2011.) (Revised by Mario Carneiro, 9-Oct-2016.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐴 ∣ 𝜓} | ||
Theorem | cbvrabv 2738* | Rule to change the bound variable in a restricted class abstraction, using implicit substitution. (Contributed by NM, 26-May-1999.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐴 ∣ 𝜓} | ||
Syntax | cvv 2739 | Extend class notation to include the universal class symbol. |
class V | ||
Theorem | vjust 2740 | Soundness justification theorem for df-v 2741. (Contributed by Rodolfo Medina, 27-Apr-2010.) |
⊢ {𝑥 ∣ 𝑥 = 𝑥} = {𝑦 ∣ 𝑦 = 𝑦} | ||
Definition | df-v 2741 | Define the universal class. Definition 5.20 of [TakeutiZaring] p. 21. Also Definition 2.9 of [Quine] p. 19. (Contributed by NM, 5-Aug-1993.) |
⊢ V = {𝑥 ∣ 𝑥 = 𝑥} | ||
Theorem | vex 2742 | All setvar variables are sets (see isset 2745). Theorem 6.8 of [Quine] p. 43. (Contributed by NM, 5-Aug-1993.) |
⊢ 𝑥 ∈ V | ||
Theorem | elv 2743 | Technical lemma used to shorten proofs. If a proposition is implied by 𝑥 ∈ V (which is true, see vex 2742), then it is true. (Contributed by Peter Mazsa, 13-Oct-2018.) |
⊢ (𝑥 ∈ V → 𝜑) ⇒ ⊢ 𝜑 | ||
Theorem | elvd 2744 | Technical lemma used to shorten proofs. If a proposition is implied by 𝑥 ∈ V (which is true, see vex 2742) and another antecedent, then it is implied by the other antecedent. (Contributed by Peter Mazsa, 23-Oct-2018.) |
⊢ ((𝜑 ∧ 𝑥 ∈ V) → 𝜓) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | isset 2745* |
Two ways to say "𝐴 is a set": A class 𝐴 is a
member of the
universal class V (see df-v 2741)
if and only if the class 𝐴
exists (i.e. there exists some set 𝑥 equal to class 𝐴).
Theorem 6.9 of [Quine] p. 43.
Notational convention: We will use the
notational device "𝐴 ∈ V " to mean "𝐴 is a
set" very
frequently, for example in uniex 4439. Note the when 𝐴 is not
a set,
it is called a proper class. In some theorems, such as uniexg 4441, in
order to shorten certain proofs we use the more general antecedent
𝐴
∈ 𝑉 instead of
𝐴 ∈
V to mean "𝐴 is a set."
Note that a constant is implicitly considered distinct from all variables. This is why V is not included in the distinct variable list, even though df-clel 2173 requires that the expression substituted for 𝐵 not contain 𝑥. (Also, the Metamath spec does not allow constants in the distinct variable list.) (Contributed by NM, 26-May-1993.) |
⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴) | ||
Theorem | issetf 2746 | A version of isset that does not require x and A to be distinct. (Contributed by Andrew Salmon, 6-Jun-2011.) (Revised by Mario Carneiro, 10-Oct-2016.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴) | ||
Theorem | isseti 2747* | A way to say "𝐴 is a set" (inference form). (Contributed by NM, 5-Aug-1993.) |
⊢ 𝐴 ∈ V ⇒ ⊢ ∃𝑥 𝑥 = 𝐴 | ||
Theorem | issetri 2748* | A way to say "𝐴 is a set" (inference form). (Contributed by NM, 5-Aug-1993.) |
⊢ ∃𝑥 𝑥 = 𝐴 ⇒ ⊢ 𝐴 ∈ V | ||
Theorem | eqvisset 2749 | A class equal to a variable is a set. Note the absence of disjoint variable condition, contrary to isset 2745 and issetri 2748. (Contributed by BJ, 27-Apr-2019.) |
⊢ (𝑥 = 𝐴 → 𝐴 ∈ V) | ||
Theorem | elex 2750 | If a class is a member of another class, then it is a set. Theorem 6.12 of [Quine] p. 44. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) |
⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V) | ||
Theorem | elexi 2751 | If a class is a member of another class, it is a set. (Contributed by NM, 11-Jun-1994.) |
⊢ 𝐴 ∈ 𝐵 ⇒ ⊢ 𝐴 ∈ V | ||
Theorem | elexd 2752 | If a class is a member of another class, it is a set. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → 𝐴 ∈ V) | ||
Theorem | elisset 2753* | An element of a class exists. (Contributed by NM, 1-May-1995.) |
⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴) | ||
Theorem | elex22 2754* | If two classes each contain another class, then both contain some set. (Contributed by Alan Sare, 24-Oct-2011.) |
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶) → ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)) | ||
Theorem | elex2 2755* | If a class contains another class, then it contains some set. (Contributed by Alan Sare, 25-Sep-2011.) |
⊢ (𝐴 ∈ 𝐵 → ∃𝑥 𝑥 ∈ 𝐵) | ||
Theorem | ralv 2756 | A universal quantifier restricted to the universe is unrestricted. (Contributed by NM, 26-Mar-2004.) |
⊢ (∀𝑥 ∈ V 𝜑 ↔ ∀𝑥𝜑) | ||
Theorem | rexv 2757 | An existential quantifier restricted to the universe is unrestricted. (Contributed by NM, 26-Mar-2004.) |
⊢ (∃𝑥 ∈ V 𝜑 ↔ ∃𝑥𝜑) | ||
Theorem | reuv 2758 | A unique existential quantifier restricted to the universe is unrestricted. (Contributed by NM, 1-Nov-2010.) |
⊢ (∃!𝑥 ∈ V 𝜑 ↔ ∃!𝑥𝜑) | ||
Theorem | rmov 2759 | An at-most-one quantifier restricted to the universe is unrestricted. (Contributed by Alexander van der Vekens, 17-Jun-2017.) |
⊢ (∃*𝑥 ∈ V 𝜑 ↔ ∃*𝑥𝜑) | ||
Theorem | rabab 2760 | A class abstraction restricted to the universe is unrestricted. (Contributed by NM, 27-Dec-2004.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) |
⊢ {𝑥 ∈ V ∣ 𝜑} = {𝑥 ∣ 𝜑} | ||
Theorem | ralcom4 2761* | Commutation of restricted and unrestricted universal quantifiers. (Contributed by NM, 26-Mar-2004.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) |
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦𝜑 ↔ ∀𝑦∀𝑥 ∈ 𝐴 𝜑) | ||
Theorem | rexcom4 2762* | Commutation of restricted and unrestricted existential quantifiers. (Contributed by NM, 12-Apr-2004.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) |
⊢ (∃𝑥 ∈ 𝐴 ∃𝑦𝜑 ↔ ∃𝑦∃𝑥 ∈ 𝐴 𝜑) | ||
Theorem | rexcom4a 2763* | Specialized existential commutation lemma. (Contributed by Jeff Madsen, 1-Jun-2011.) |
⊢ (∃𝑥∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ ∃𝑦 ∈ 𝐴 (𝜑 ∧ ∃𝑥𝜓)) | ||
Theorem | rexcom4b 2764* | Specialized existential commutation lemma. (Contributed by Jeff Madsen, 1-Jun-2011.) |
⊢ 𝐵 ∈ V ⇒ ⊢ (∃𝑥∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵) ↔ ∃𝑦 ∈ 𝐴 𝜑) | ||
Theorem | ceqsalt 2765* | Closed theorem version of ceqsalg 2767. (Contributed by NM, 28-Feb-2013.) (Revised by Mario Carneiro, 10-Oct-2016.) |
⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝑉) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓)) | ||
Theorem | ceqsralt 2766* | Restricted quantifier version of ceqsalt 2765. (Contributed by NM, 28-Feb-2013.) (Revised by Mario Carneiro, 10-Oct-2016.) |
⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝐵) → (∀𝑥 ∈ 𝐵 (𝑥 = 𝐴 → 𝜑) ↔ 𝜓)) | ||
Theorem | ceqsalg 2767* | A representation of explicit substitution of a class for a variable, inferred from an implicit substitution hypothesis. (Contributed by NM, 29-Oct-2003.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓)) | ||
Theorem | ceqsal 2768* | A representation of explicit substitution of a class for a variable, inferred from an implicit substitution hypothesis. (Contributed by NM, 18-Aug-1993.) |
⊢ Ⅎ𝑥𝜓 & ⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓) | ||
Theorem | ceqsalv 2769* | A representation of explicit substitution of a class for a variable, inferred from an implicit substitution hypothesis. (Contributed by NM, 18-Aug-1993.) |
⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓) | ||
Theorem | ceqsralv 2770* | Restricted quantifier version of ceqsalv 2769. (Contributed by NM, 21-Jun-2013.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 (𝑥 = 𝐴 → 𝜑) ↔ 𝜓)) | ||
Theorem | gencl 2771* | Implicit substitution for class with embedded variable. (Contributed by NM, 17-May-1996.) |
⊢ (𝜃 ↔ ∃𝑥(𝜒 ∧ 𝐴 = 𝐵)) & ⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜓)) & ⊢ (𝜒 → 𝜑) ⇒ ⊢ (𝜃 → 𝜓) | ||
Theorem | 2gencl 2772* | Implicit substitution for class with embedded variable. (Contributed by NM, 17-May-1996.) |
⊢ (𝐶 ∈ 𝑆 ↔ ∃𝑥 ∈ 𝑅 𝐴 = 𝐶) & ⊢ (𝐷 ∈ 𝑆 ↔ ∃𝑦 ∈ 𝑅 𝐵 = 𝐷) & ⊢ (𝐴 = 𝐶 → (𝜑 ↔ 𝜓)) & ⊢ (𝐵 = 𝐷 → (𝜓 ↔ 𝜒)) & ⊢ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅) → 𝜑) ⇒ ⊢ ((𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆) → 𝜒) | ||
Theorem | 3gencl 2773* | Implicit substitution for class with embedded variable. (Contributed by NM, 17-May-1996.) |
⊢ (𝐷 ∈ 𝑆 ↔ ∃𝑥 ∈ 𝑅 𝐴 = 𝐷) & ⊢ (𝐹 ∈ 𝑆 ↔ ∃𝑦 ∈ 𝑅 𝐵 = 𝐹) & ⊢ (𝐺 ∈ 𝑆 ↔ ∃𝑧 ∈ 𝑅 𝐶 = 𝐺) & ⊢ (𝐴 = 𝐷 → (𝜑 ↔ 𝜓)) & ⊢ (𝐵 = 𝐹 → (𝜓 ↔ 𝜒)) & ⊢ (𝐶 = 𝐺 → (𝜒 ↔ 𝜃)) & ⊢ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅) → 𝜑) ⇒ ⊢ ((𝐷 ∈ 𝑆 ∧ 𝐹 ∈ 𝑆 ∧ 𝐺 ∈ 𝑆) → 𝜃) | ||
Theorem | cgsexg 2774* | Implicit substitution inference for general classes. (Contributed by NM, 26-Aug-2007.) |
⊢ (𝑥 = 𝐴 → 𝜒) & ⊢ (𝜒 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (∃𝑥(𝜒 ∧ 𝜑) ↔ 𝜓)) | ||
Theorem | cgsex2g 2775* | Implicit substitution inference for general classes. (Contributed by NM, 26-Jul-1995.) |
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → 𝜒) & ⊢ (𝜒 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∃𝑥∃𝑦(𝜒 ∧ 𝜑) ↔ 𝜓)) | ||
Theorem | cgsex4g 2776* | An implicit substitution inference for 4 general classes. (Contributed by NM, 5-Aug-1995.) |
⊢ (((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑤 = 𝐷)) → 𝜒) & ⊢ (𝜒 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑅 ∧ 𝐷 ∈ 𝑆)) → (∃𝑥∃𝑦∃𝑧∃𝑤(𝜒 ∧ 𝜑) ↔ 𝜓)) | ||
Theorem | ceqsex 2777* | Elimination of an existential quantifier, using implicit substitution. (Contributed by NM, 2-Mar-1995.) (Revised by Mario Carneiro, 10-Oct-2016.) |
⊢ Ⅎ𝑥𝜓 & ⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥(𝑥 = 𝐴 ∧ 𝜑) ↔ 𝜓) | ||
Theorem | ceqsexv 2778* | Elimination of an existential quantifier, using implicit substitution. (Contributed by NM, 2-Mar-1995.) |
⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥(𝑥 = 𝐴 ∧ 𝜑) ↔ 𝜓) | ||
Theorem | ceqsex2 2779* | Elimination of two existential quantifiers, using implicit substitution. (Contributed by Scott Fenton, 7-Jun-2006.) |
⊢ Ⅎ𝑥𝜓 & ⊢ Ⅎ𝑦𝜒 & ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (∃𝑥∃𝑦(𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝜑) ↔ 𝜒) | ||
Theorem | ceqsex2v 2780* | Elimination of two existential quantifiers, using implicit substitution. (Contributed by Scott Fenton, 7-Jun-2006.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (∃𝑥∃𝑦(𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝜑) ↔ 𝜒) | ||
Theorem | ceqsex3v 2781* | Elimination of three existential quantifiers, using implicit substitution. (Contributed by NM, 16-Aug-2011.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ (𝑧 = 𝐶 → (𝜒 ↔ 𝜃)) ⇒ ⊢ (∃𝑥∃𝑦∃𝑧((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) ∧ 𝜑) ↔ 𝜃) | ||
Theorem | ceqsex4v 2782* | Elimination of four existential quantifiers, using implicit substitution. (Contributed by NM, 23-Sep-2011.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ 𝐷 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ (𝑧 = 𝐶 → (𝜒 ↔ 𝜃)) & ⊢ (𝑤 = 𝐷 → (𝜃 ↔ 𝜏)) ⇒ ⊢ (∃𝑥∃𝑦∃𝑧∃𝑤((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑤 = 𝐷) ∧ 𝜑) ↔ 𝜏) | ||
Theorem | ceqsex6v 2783* | Elimination of six existential quantifiers, using implicit substitution. (Contributed by NM, 21-Sep-2011.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ 𝐷 ∈ V & ⊢ 𝐸 ∈ V & ⊢ 𝐹 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ (𝑧 = 𝐶 → (𝜒 ↔ 𝜃)) & ⊢ (𝑤 = 𝐷 → (𝜃 ↔ 𝜏)) & ⊢ (𝑣 = 𝐸 → (𝜏 ↔ 𝜂)) & ⊢ (𝑢 = 𝐹 → (𝜂 ↔ 𝜁)) ⇒ ⊢ (∃𝑥∃𝑦∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) ∧ (𝑤 = 𝐷 ∧ 𝑣 = 𝐸 ∧ 𝑢 = 𝐹) ∧ 𝜑) ↔ 𝜁) | ||
Theorem | ceqsex8v 2784* | Elimination of eight existential quantifiers, using implicit substitution. (Contributed by NM, 23-Sep-2011.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ 𝐷 ∈ V & ⊢ 𝐸 ∈ V & ⊢ 𝐹 ∈ V & ⊢ 𝐺 ∈ V & ⊢ 𝐻 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ (𝑧 = 𝐶 → (𝜒 ↔ 𝜃)) & ⊢ (𝑤 = 𝐷 → (𝜃 ↔ 𝜏)) & ⊢ (𝑣 = 𝐸 → (𝜏 ↔ 𝜂)) & ⊢ (𝑢 = 𝐹 → (𝜂 ↔ 𝜁)) & ⊢ (𝑡 = 𝐺 → (𝜁 ↔ 𝜎)) & ⊢ (𝑠 = 𝐻 → (𝜎 ↔ 𝜌)) ⇒ ⊢ (∃𝑥∃𝑦∃𝑧∃𝑤∃𝑣∃𝑢∃𝑡∃𝑠(((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑤 = 𝐷)) ∧ ((𝑣 = 𝐸 ∧ 𝑢 = 𝐹) ∧ (𝑡 = 𝐺 ∧ 𝑠 = 𝐻)) ∧ 𝜑) ↔ 𝜌) | ||
Theorem | gencbvex 2785* | Change of bound variable using implicit substitution. (Contributed by NM, 17-May-1996.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) |
⊢ 𝐴 ∈ V & ⊢ (𝐴 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ (𝐴 = 𝑦 → (𝜒 ↔ 𝜃)) & ⊢ (𝜃 ↔ ∃𝑥(𝜒 ∧ 𝐴 = 𝑦)) ⇒ ⊢ (∃𝑥(𝜒 ∧ 𝜑) ↔ ∃𝑦(𝜃 ∧ 𝜓)) | ||
Theorem | gencbvex2 2786* | Restatement of gencbvex 2785 with weaker hypotheses. (Contributed by Jeff Hankins, 6-Dec-2006.) |
⊢ 𝐴 ∈ V & ⊢ (𝐴 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ (𝐴 = 𝑦 → (𝜒 ↔ 𝜃)) & ⊢ (𝜃 → ∃𝑥(𝜒 ∧ 𝐴 = 𝑦)) ⇒ ⊢ (∃𝑥(𝜒 ∧ 𝜑) ↔ ∃𝑦(𝜃 ∧ 𝜓)) | ||
Theorem | gencbval 2787* | Change of bound variable using implicit substitution. (Contributed by NM, 17-May-1996.) (Proof rewritten by Jim Kingdon, 20-Jun-2018.) |
⊢ 𝐴 ∈ V & ⊢ (𝐴 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ (𝐴 = 𝑦 → (𝜒 ↔ 𝜃)) & ⊢ (𝜃 ↔ ∃𝑥(𝜒 ∧ 𝐴 = 𝑦)) ⇒ ⊢ (∀𝑥(𝜒 → 𝜑) ↔ ∀𝑦(𝜃 → 𝜓)) | ||
Theorem | sbhypf 2788* | Introduce an explicit substitution into an implicit substitution hypothesis. See also csbhypf . (Contributed by Raph Levien, 10-Apr-2004.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ 𝜓)) | ||
Theorem | vtoclgft 2789 | Closed theorem form of vtoclgf 2797. (Contributed by NM, 17-Feb-2013.) (Revised by Mario Carneiro, 12-Oct-2016.) |
⊢ (((Ⅎ𝑥𝐴 ∧ Ⅎ𝑥𝜓) ∧ (∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∀𝑥𝜑) ∧ 𝐴 ∈ 𝑉) → 𝜓) | ||
Theorem | vtocldf 2790 | Implicit substitution of a class for a setvar variable. (Contributed by Mario Carneiro, 15-Oct-2016.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → 𝜓) & ⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝐴) & ⊢ (𝜑 → Ⅎ𝑥𝜒) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | vtocld 2791* | Implicit substitution of a class for a setvar variable. (Contributed by Mario Carneiro, 15-Oct-2016.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → 𝜓) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | vtoclf 2792* | Implicit substitution of a class for a setvar variable. This is a generalization of chvar 1757. (Contributed by NM, 30-Aug-1993.) |
⊢ Ⅎ𝑥𝜓 & ⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ 𝜑 ⇒ ⊢ 𝜓 | ||
Theorem | vtocl 2793* | Implicit substitution of a class for a setvar variable. (Contributed by NM, 30-Aug-1993.) |
⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ 𝜑 ⇒ ⊢ 𝜓 | ||
Theorem | vtocl2 2794* | Implicit substitution of classes for setvar variables. (Contributed by NM, 26-Jul-1995.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) & ⊢ 𝜑 ⇒ ⊢ 𝜓 | ||
Theorem | vtocl3 2795* | Implicit substitution of classes for setvar variables. (Contributed by NM, 3-Jun-1995.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) → (𝜑 ↔ 𝜓)) & ⊢ 𝜑 ⇒ ⊢ 𝜓 | ||
Theorem | vtoclb 2796* | Implicit substitution of a class for a setvar variable. (Contributed by NM, 23-Dec-1993.) |
⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜃)) & ⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (𝜒 ↔ 𝜃) | ||
Theorem | vtoclgf 2797 | Implicit substitution of a class for a setvar variable, with bound-variable hypotheses in place of distinct variable restrictions. (Contributed by NM, 21-Sep-2003.) (Proof shortened by Mario Carneiro, 10-Oct-2016.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ 𝜑 ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝜓) | ||
Theorem | vtoclg1f 2798* | Version of vtoclgf 2797 with one nonfreeness hypothesis replaced with a disjoint variable condition, thus avoiding dependency on ax-11 1506 and ax-13 2150. (Contributed by BJ, 1-May-2019.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ 𝜑 ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝜓) | ||
Theorem | vtoclg 2799* | Implicit substitution of a class expression for a setvar variable. (Contributed by NM, 17-Apr-1995.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ 𝜑 ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝜓) | ||
Theorem | vtoclbg 2800* | Implicit substitution of a class for a setvar variable. (Contributed by NM, 29-Apr-1994.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜃)) & ⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (𝐴 ∈ 𝑉 → (𝜒 ↔ 𝜃)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |