Theorem List for Intuitionistic Logic Explorer - 2601-2700 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | rexlimiv 2601* |
Inference from Theorem 19.23 of [Margaris] p.
90. (Restricted
quantifier version.) (Contributed by NM, 20-Nov-1994.)
|
⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓) |
|
Theorem | rexlimiva 2602* |
Inference from Theorem 19.23 of [Margaris] p.
90 (restricted quantifier
version). (Contributed by NM, 18-Dec-2006.)
|
⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝜓) ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓) |
|
Theorem | rexlimivw 2603* |
Weaker version of rexlimiv 2601. (Contributed by FL, 19-Sep-2011.)
|
⊢ (𝜑 → 𝜓) ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓) |
|
Theorem | rexlimd 2604 |
Deduction from Theorem 19.23 of [Margaris] p.
90 (restricted quantifier
version). (Contributed by NM, 27-May-1998.) (Proof shortened by Andrew
Salmon, 30-May-2011.)
|
⊢ Ⅎ𝑥𝜑
& ⊢ Ⅎ𝑥𝜒
& ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒))) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒)) |
|
Theorem | rexlimd2 2605 |
Version of rexlimd 2604 with deduction version of second hypothesis.
(Contributed by NM, 21-Jul-2013.) (Revised by Mario Carneiro,
8-Oct-2016.)
|
⊢ Ⅎ𝑥𝜑
& ⊢ (𝜑 → Ⅎ𝑥𝜒)
& ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒))) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒)) |
|
Theorem | rexlimdv 2606* |
Inference from Theorem 19.23 of [Margaris] p.
90 (restricted quantifier
version). (Contributed by NM, 14-Nov-2002.) (Proof shortened by Eric
Schmidt, 22-Dec-2006.)
|
⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒))) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒)) |
|
Theorem | rexlimdva 2607* |
Inference from Theorem 19.23 of [Margaris] p.
90 (restricted quantifier
version). (Contributed by NM, 20-Jan-2007.)
|
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒)) |
|
Theorem | rexlimdvaa 2608* |
Inference from Theorem 19.23 of [Margaris] p.
90 (restricted quantifier
version). (Contributed by Mario Carneiro, 15-Jun-2016.)
|
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝜓)) → 𝜒) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒)) |
|
Theorem | rexlimdv3a 2609* |
Inference from Theorem 19.23 of [Margaris] p.
90 (restricted quantifier
version). Frequently-used variant of rexlimdv 2606. (Contributed by NM,
7-Jun-2015.)
|
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝜓) → 𝜒) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒)) |
|
Theorem | rexlimdva2 2610* |
Inference from Theorem 19.23 of [Margaris] p.
90 (restricted quantifier
version). (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) → 𝜒) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒)) |
|
Theorem | rexlimdvw 2611* |
Inference from Theorem 19.23 of [Margaris] p.
90 (restricted quantifier
version). (Contributed by NM, 18-Jun-2014.)
|
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒)) |
|
Theorem | rexlimddv 2612* |
Restricted existential elimination rule of natural deduction.
(Contributed by Mario Carneiro, 15-Jun-2016.)
|
⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓)
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝜓)) → 𝜒) ⇒ ⊢ (𝜑 → 𝜒) |
|
Theorem | rexlimivv 2613* |
Inference from Theorem 19.23 of [Margaris] p.
90 (restricted quantifier
version). (Contributed by NM, 17-Feb-2004.)
|
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝜑 → 𝜓)) ⇒ ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 → 𝜓) |
|
Theorem | rexlimdvv 2614* |
Inference from Theorem 19.23 of [Margaris] p.
90. (Restricted
quantifier version.) (Contributed by NM, 22-Jul-2004.)
|
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝜓 → 𝜒))) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 → 𝜒)) |
|
Theorem | rexlimdvva 2615* |
Inference from Theorem 19.23 of [Margaris] p.
90. (Restricted
quantifier version.) (Contributed by NM, 18-Jun-2014.)
|
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 → 𝜒)) |
|
Theorem | r19.26 2616 |
Theorem 19.26 of [Margaris] p. 90 with
restricted quantifiers.
(Contributed by NM, 28-Jan-1997.) (Proof shortened by Andrew Salmon,
30-May-2011.)
|
⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓)) |
|
Theorem | r19.27v 2617* |
Restricted quantitifer version of one direction of 19.27 1572. (The other
direction holds when 𝐴 is inhabited, see r19.27mv 3534.) (Contributed
by NM, 3-Jun-2004.) (Proof shortened by Andrew Salmon, 30-May-2011.)
(Proof shortened by Wolf Lammen, 17-Jun-2023.)
|
⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ 𝜓) → ∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)) |
|
Theorem | r19.28v 2618* |
Restricted quantifier version of one direction of 19.28 1574. (The other
direction holds when 𝐴 is inhabited, see r19.28mv 3530.) (Contributed
by NM, 2-Apr-2004.) (Proof shortened by Wolf Lammen, 17-Jun-2023.)
|
⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) → ∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)) |
|
Theorem | r19.26-2 2619 |
Theorem 19.26 of [Margaris] p. 90 with 2
restricted quantifiers.
(Contributed by NM, 10-Aug-2004.)
|
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓)) |
|
Theorem | r19.26-3 2620 |
Theorem 19.26 of [Margaris] p. 90 with 3
restricted quantifiers.
(Contributed by FL, 22-Nov-2010.)
|
⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓 ∧ ∀𝑥 ∈ 𝐴 𝜒)) |
|
Theorem | r19.26m 2621 |
Theorem 19.26 of [Margaris] p. 90 with mixed
quantifiers. (Contributed by
NM, 22-Feb-2004.)
|
⊢ (∀𝑥((𝑥 ∈ 𝐴 → 𝜑) ∧ (𝑥 ∈ 𝐵 → 𝜓)) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐵 𝜓)) |
|
Theorem | ralbi 2622 |
Distribute a restricted universal quantifier over a biconditional.
Theorem 19.15 of [Margaris] p. 90 with
restricted quantification.
(Contributed by NM, 6-Oct-2003.)
|
⊢ (∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓)) |
|
Theorem | rexbi 2623 |
Distribute a restricted existential quantifier over a biconditional.
Theorem 19.18 of [Margaris] p. 90 with
restricted quantification.
(Contributed by Jim Kingdon, 21-Jan-2019.)
|
⊢ (∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓) → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐴 𝜓)) |
|
Theorem | ralbiim 2624 |
Split a biconditional and distribute quantifier. (Contributed by NM,
3-Jun-2012.)
|
⊢ (∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓) ↔ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ∧ ∀𝑥 ∈ 𝐴 (𝜓 → 𝜑))) |
|
Theorem | r19.27av 2625* |
Restricted version of one direction of Theorem 19.27 of [Margaris]
p. 90. (The other direction doesn't hold when 𝐴 is empty.)
(Contributed by NM, 3-Jun-2004.) (Proof shortened by Andrew Salmon,
30-May-2011.)
|
⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ 𝜓) → ∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)) |
|
Theorem | r19.28av 2626* |
Restricted version of one direction of Theorem 19.28 of [Margaris]
p. 90. (The other direction doesn't hold when 𝐴 is empty.)
(Contributed by NM, 2-Apr-2004.)
|
⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) → ∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)) |
|
Theorem | r19.29 2627 |
Theorem 19.29 of [Margaris] p. 90 with
restricted quantifiers.
(Contributed by NM, 31-Aug-1999.) (Proof shortened by Andrew Salmon,
30-May-2011.)
|
⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓) → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)) |
|
Theorem | r19.29r 2628 |
Variation of Theorem 19.29 of [Margaris] p. 90
with restricted
quantifiers. (Contributed by NM, 31-Aug-1999.)
|
⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)) |
|
Theorem | ralnex2 2629 |
Relationship between two restricted universal and existential quantifiers.
(Contributed by Glauco Siliprandi, 11-Dec-2019.) (Proof shortened by Wolf
Lammen, 18-May-2023.)
|
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ¬ 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) |
|
Theorem | r19.29af2 2630 |
A commonly used pattern based on r19.29 2627. (Contributed by Thierry
Arnoux, 17-Dec-2017.)
|
⊢ Ⅎ𝑥𝜑
& ⊢ Ⅎ𝑥𝜒
& ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) → 𝜒)
& ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓) ⇒ ⊢ (𝜑 → 𝜒) |
|
Theorem | r19.29af 2631* |
A commonly used pattern based on r19.29 2627. (Contributed by Thierry
Arnoux, 29-Nov-2017.)
|
⊢ Ⅎ𝑥𝜑
& ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) → 𝜒)
& ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓) ⇒ ⊢ (𝜑 → 𝜒) |
|
Theorem | r19.29an 2632* |
A commonly used pattern based on r19.29 2627. (Contributed by Thierry
Arnoux, 29-Dec-2019.)
|
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) → 𝜒) ⇒ ⊢ ((𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓) → 𝜒) |
|
Theorem | r19.29a 2633* |
A commonly used pattern based on r19.29 2627. (Contributed by Thierry
Arnoux, 22-Nov-2017.)
|
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) → 𝜒)
& ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓) ⇒ ⊢ (𝜑 → 𝜒) |
|
Theorem | r19.29d2r 2634 |
Theorem 19.29 of [Margaris] p. 90 with two
restricted quantifiers,
deduction version. (Contributed by Thierry Arnoux, 30-Jan-2017.)
|
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓)
& ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜓 ∧ 𝜒)) |
|
Theorem | r19.29vva 2635* |
A commonly used pattern based on r19.29 2627, version with two restricted
quantifiers. (Contributed by Thierry Arnoux, 26-Nov-2017.)
|
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ 𝜓) → 𝜒)
& ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓) ⇒ ⊢ (𝜑 → 𝜒) |
|
Theorem | r19.32r 2636 |
One direction of Theorem 19.32 of [Margaris]
p. 90 with restricted
quantifiers. For decidable propositions this is an equivalence.
(Contributed by Jim Kingdon, 19-Aug-2018.)
|
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ ((𝜑 ∨ ∀𝑥 ∈ 𝐴 𝜓) → ∀𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓)) |
|
Theorem | r19.30dc 2637 |
Restricted quantifier version of 19.30dc 1638. (Contributed by Scott
Fenton, 25-Feb-2011.) (Proof shortened by Wolf Lammen, 18-Jun-2023.)
|
⊢ ((∀𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓) ∧ DECID ∃𝑥 ∈ 𝐴 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 ∨ ∃𝑥 ∈ 𝐴 𝜓)) |
|
Theorem | r19.32vr 2638* |
One direction of Theorem 19.32 of [Margaris]
p. 90 with restricted
quantifiers. For decidable propositions this is an equivalence, as seen
at r19.32vdc 2639. (Contributed by Jim Kingdon, 19-Aug-2018.)
|
⊢ ((𝜑 ∨ ∀𝑥 ∈ 𝐴 𝜓) → ∀𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓)) |
|
Theorem | r19.32vdc 2639* |
Theorem 19.32 of [Margaris] p. 90 with
restricted quantifiers, where
𝜑 is decidable. (Contributed by Jim
Kingdon, 4-Jun-2018.)
|
⊢ (DECID 𝜑 → (∀𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓) ↔ (𝜑 ∨ ∀𝑥 ∈ 𝐴 𝜓))) |
|
Theorem | r19.35-1 2640 |
Restricted quantifier version of 19.35-1 1635. (Contributed by Jim Kingdon,
4-Jun-2018.)
|
⊢ (∃𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓)) |
|
Theorem | r19.36av 2641* |
One direction of a restricted quantifier version of Theorem 19.36 of
[Margaris] p. 90. In classical logic,
the converse would hold if 𝐴
has at least one element, but in intuitionistic logic, that is not a
sufficient condition. (Contributed by NM, 22-Oct-2003.)
|
⊢ (∃𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 → 𝜓)) |
|
Theorem | r19.37 2642 |
Restricted version of one direction of Theorem 19.37 of [Margaris]
p. 90. In classical logic the converse would hold if 𝐴 has at
least
one element, but that is not sufficient in intuitionistic logic.
(Contributed by FL, 13-May-2012.) (Revised by Mario Carneiro,
11-Dec-2016.)
|
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (∃𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (𝜑 → ∃𝑥 ∈ 𝐴 𝜓)) |
|
Theorem | r19.37av 2643* |
Restricted version of one direction of Theorem 19.37 of [Margaris]
p. 90. (Contributed by NM, 2-Apr-2004.)
|
⊢ (∃𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (𝜑 → ∃𝑥 ∈ 𝐴 𝜓)) |
|
Theorem | r19.40 2644 |
Restricted quantifier version of Theorem 19.40 of [Margaris] p. 90.
(Contributed by NM, 2-Apr-2004.)
|
⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓)) |
|
Theorem | r19.41 2645 |
Restricted quantifier version of Theorem 19.41 of [Margaris] p. 90.
(Contributed by NM, 1-Nov-2010.)
|
⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ 𝜓)) |
|
Theorem | r19.41v 2646* |
Restricted quantifier version of Theorem 19.41 of [Margaris] p. 90.
(Contributed by NM, 17-Dec-2003.)
|
⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ 𝜓)) |
|
Theorem | r19.42v 2647* |
Restricted version of Theorem 19.42 of [Margaris] p. 90. (Contributed
by NM, 27-May-1998.)
|
⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓)) |
|
Theorem | r19.43 2648 |
Restricted version of Theorem 19.43 of [Margaris] p. 90. (Contributed by
NM, 27-May-1998.) (Proof rewritten by Jim Kingdon, 5-Jun-2018.)
|
⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∨ ∃𝑥 ∈ 𝐴 𝜓)) |
|
Theorem | r19.44av 2649* |
One direction of a restricted quantifier version of Theorem 19.44 of
[Margaris] p. 90. The other direction
doesn't hold when 𝐴 is empty.
(Contributed by NM, 2-Apr-2004.)
|
⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓) → (∃𝑥 ∈ 𝐴 𝜑 ∨ 𝜓)) |
|
Theorem | r19.45av 2650* |
Restricted version of one direction of Theorem 19.45 of [Margaris]
p. 90. (The other direction doesn't hold when 𝐴 is empty.)
(Contributed by NM, 2-Apr-2004.)
|
⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓) → (𝜑 ∨ ∃𝑥 ∈ 𝐴 𝜓)) |
|
Theorem | ralcomf 2651* |
Commutation of restricted quantifiers. (Contributed by Mario Carneiro,
14-Oct-2016.)
|
⊢ Ⅎ𝑦𝐴
& ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 𝜑) |
|
Theorem | rexcomf 2652* |
Commutation of restricted quantifiers. (Contributed by Mario Carneiro,
14-Oct-2016.)
|
⊢ Ⅎ𝑦𝐴
& ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) |
|
Theorem | ralcom 2653* |
Commutation of restricted quantifiers. (Contributed by NM,
13-Oct-1999.) (Revised by Mario Carneiro, 14-Oct-2016.)
|
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 𝜑) |
|
Theorem | rexcom 2654* |
Commutation of restricted quantifiers. (Contributed by NM,
19-Nov-1995.) (Revised by Mario Carneiro, 14-Oct-2016.)
|
⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) |
|
Theorem | ralrot3 2655* |
Rotate three restricted universal quantifiers. (Contributed by AV,
3-Dec-2021.)
|
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜑 ↔ ∀𝑧 ∈ 𝐶 ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑) |
|
Theorem | rexcom13 2656* |
Swap 1st and 3rd restricted existential quantifiers. (Contributed by
NM, 8-Apr-2015.)
|
⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐶 𝜑 ↔ ∃𝑧 ∈ 𝐶 ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) |
|
Theorem | rexrot4 2657* |
Rotate existential restricted quantifiers twice. (Contributed by NM,
8-Apr-2015.)
|
⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐶 ∃𝑤 ∈ 𝐷 𝜑 ↔ ∃𝑧 ∈ 𝐶 ∃𝑤 ∈ 𝐷 ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) |
|
Theorem | ralcom3 2658 |
A commutative law for restricted quantifiers that swaps the domain of the
restriction. (Contributed by NM, 22-Feb-2004.)
|
⊢ (∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝐵 → 𝜑) ↔ ∀𝑥 ∈ 𝐵 (𝑥 ∈ 𝐴 → 𝜑)) |
|
Theorem | reean 2659* |
Rearrange existential quantifiers. (Contributed by NM, 27-Oct-2010.)
(Proof shortened by Andrew Salmon, 30-May-2011.)
|
⊢ Ⅎ𝑦𝜑
& ⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐵 𝜓)) |
|
Theorem | reeanv 2660* |
Rearrange existential quantifiers. (Contributed by NM, 9-May-1999.)
|
⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐵 𝜓)) |
|
Theorem | 3reeanv 2661* |
Rearrange three existential quantifiers. (Contributed by Jeff Madsen,
11-Jun-2010.)
|
⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐶 (𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐵 𝜓 ∧ ∃𝑧 ∈ 𝐶 𝜒)) |
|
Theorem | nfreu1 2662 |
𝑥
is not free in ∃!𝑥 ∈ 𝐴𝜑. (Contributed by NM,
19-Mar-1997.)
|
⊢ Ⅎ𝑥∃!𝑥 ∈ 𝐴 𝜑 |
|
Theorem | nfrmo1 2663 |
𝑥
is not free in ∃*𝑥 ∈ 𝐴𝜑. (Contributed by NM,
16-Jun-2017.)
|
⊢ Ⅎ𝑥∃*𝑥 ∈ 𝐴 𝜑 |
|
Theorem | nfreudxy 2664* |
Not-free deduction for restricted uniqueness. This is a version where
𝑥 and 𝑦 are distinct.
(Contributed by Jim Kingdon,
6-Jun-2018.)
|
⊢ Ⅎ𝑦𝜑
& ⊢ (𝜑 → Ⅎ𝑥𝐴)
& ⊢ (𝜑 → Ⅎ𝑥𝜓) ⇒ ⊢ (𝜑 → Ⅎ𝑥∃!𝑦 ∈ 𝐴 𝜓) |
|
Theorem | nfreuxy 2665* |
Not-free for restricted uniqueness. This is a version where 𝑥 and
𝑦 are distinct. (Contributed by Jim
Kingdon, 6-Jun-2018.)
|
⊢ Ⅎ𝑥𝐴
& ⊢ Ⅎ𝑥𝜑 ⇒ ⊢ Ⅎ𝑥∃!𝑦 ∈ 𝐴 𝜑 |
|
Theorem | rabid 2666 |
An "identity" law of concretion for restricted abstraction. Special
case
of Definition 2.1 of [Quine] p. 16.
(Contributed by NM, 9-Oct-2003.)
|
⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ (𝑥 ∈ 𝐴 ∧ 𝜑)) |
|
Theorem | rabid2 2667* |
An "identity" law for restricted class abstraction. (Contributed by
NM,
9-Oct-2003.) (Proof shortened by Andrew Salmon, 30-May-2011.)
|
⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ ∀𝑥 ∈ 𝐴 𝜑) |
|
Theorem | rabbi 2668 |
Equivalent wff's correspond to equal restricted class abstractions.
Closed theorem form of rabbidva 2740. (Contributed by NM, 25-Nov-2013.)
|
⊢ (∀𝑥 ∈ 𝐴 (𝜓 ↔ 𝜒) ↔ {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒}) |
|
Theorem | rabswap 2669 |
Swap with a membership relation in a restricted class abstraction.
(Contributed by NM, 4-Jul-2005.)
|
⊢ {𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝐵} = {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝐴} |
|
Theorem | nfrab1 2670 |
The abstraction variable in a restricted class abstraction isn't free.
(Contributed by NM, 19-Mar-1997.)
|
⊢ Ⅎ𝑥{𝑥 ∈ 𝐴 ∣ 𝜑} |
|
Theorem | nfrabxy 2671* |
A variable not free in a wff remains so in a restricted class
abstraction. (Contributed by Jim Kingdon, 19-Jul-2018.)
|
⊢ Ⅎ𝑥𝜑
& ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥{𝑦 ∈ 𝐴 ∣ 𝜑} |
|
Theorem | reubida 2672 |
Formula-building rule for restricted existential quantifier (deduction
form). (Contributed by Mario Carneiro, 19-Nov-2016.)
|
⊢ Ⅎ𝑥𝜑
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐴 𝜒)) |
|
Theorem | reubidva 2673* |
Formula-building rule for restricted existential quantifier (deduction
form). (Contributed by NM, 13-Nov-2004.)
|
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐴 𝜒)) |
|
Theorem | reubidv 2674* |
Formula-building rule for restricted existential quantifier (deduction
form). (Contributed by NM, 17-Oct-1996.)
|
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐴 𝜒)) |
|
Theorem | reubiia 2675 |
Formula-building rule for restricted existential quantifier (inference
form). (Contributed by NM, 14-Nov-2004.)
|
⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥 ∈ 𝐴 𝜓) |
|
Theorem | reubii 2676 |
Formula-building rule for restricted existential quantifier (inference
form). (Contributed by NM, 22-Oct-1999.)
|
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥 ∈ 𝐴 𝜓) |
|
Theorem | rmobida 2677 |
Formula-building rule for restricted existential quantifier (deduction
form). (Contributed by NM, 16-Jun-2017.)
|
⊢ Ⅎ𝑥𝜑
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃*𝑥 ∈ 𝐴 𝜓 ↔ ∃*𝑥 ∈ 𝐴 𝜒)) |
|
Theorem | rmobidva 2678* |
Formula-building rule for restricted existential quantifier (deduction
form). (Contributed by NM, 16-Jun-2017.)
|
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃*𝑥 ∈ 𝐴 𝜓 ↔ ∃*𝑥 ∈ 𝐴 𝜒)) |
|
Theorem | rmobidv 2679* |
Formula-building rule for restricted existential quantifier (deduction
form). (Contributed by NM, 16-Jun-2017.)
|
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃*𝑥 ∈ 𝐴 𝜓 ↔ ∃*𝑥 ∈ 𝐴 𝜒)) |
|
Theorem | rmobiia 2680 |
Formula-building rule for restricted existential quantifier (inference
form). (Contributed by NM, 16-Jun-2017.)
|
⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥 ∈ 𝐴 𝜓) |
|
Theorem | rmobii 2681 |
Formula-building rule for restricted existential quantifier (inference
form). (Contributed by NM, 16-Jun-2017.)
|
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥 ∈ 𝐴 𝜓) |
|
Theorem | raleqf 2682 |
Equality theorem for restricted universal quantifier, with
bound-variable hypotheses instead of distinct variable restrictions.
(Contributed by NM, 7-Mar-2004.) (Revised by Andrew Salmon,
11-Jul-2011.)
|
⊢ Ⅎ𝑥𝐴
& ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑)) |
|
Theorem | rexeqf 2683 |
Equality theorem for restricted existential quantifier, with
bound-variable hypotheses instead of distinct variable restrictions.
(Contributed by NM, 9-Oct-2003.) (Revised by Andrew Salmon,
11-Jul-2011.)
|
⊢ Ⅎ𝑥𝐴
& ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜑)) |
|
Theorem | reueq1f 2684 |
Equality theorem for restricted unique existential quantifier, with
bound-variable hypotheses instead of distinct variable restrictions.
(Contributed by NM, 5-Apr-2004.) (Revised by Andrew Salmon,
11-Jul-2011.)
|
⊢ Ⅎ𝑥𝐴
& ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (𝐴 = 𝐵 → (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥 ∈ 𝐵 𝜑)) |
|
Theorem | rmoeq1f 2685 |
Equality theorem for restricted at-most-one quantifier, with
bound-variable hypotheses instead of distinct variable restrictions.
(Contributed by Alexander van der Vekens, 17-Jun-2017.)
|
⊢ Ⅎ𝑥𝐴
& ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (𝐴 = 𝐵 → (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥 ∈ 𝐵 𝜑)) |
|
Theorem | raleq 2686* |
Equality theorem for restricted universal quantifier. (Contributed by
NM, 16-Nov-1995.)
|
⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑)) |
|
Theorem | rexeq 2687* |
Equality theorem for restricted existential quantifier. (Contributed by
NM, 29-Oct-1995.)
|
⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜑)) |
|
Theorem | reueq1 2688* |
Equality theorem for restricted unique existential quantifier.
(Contributed by NM, 5-Apr-2004.)
|
⊢ (𝐴 = 𝐵 → (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥 ∈ 𝐵 𝜑)) |
|
Theorem | rmoeq1 2689* |
Equality theorem for restricted at-most-one quantifier. (Contributed by
Alexander van der Vekens, 17-Jun-2017.)
|
⊢ (𝐴 = 𝐵 → (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥 ∈ 𝐵 𝜑)) |
|
Theorem | raleqi 2690* |
Equality inference for restricted universal qualifier. (Contributed by
Paul Chapman, 22-Jun-2011.)
|
⊢ 𝐴 = 𝐵 ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑) |
|
Theorem | rexeqi 2691* |
Equality inference for restricted existential qualifier. (Contributed
by Mario Carneiro, 23-Apr-2015.)
|
⊢ 𝐴 = 𝐵 ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜑) |
|
Theorem | raleqdv 2692* |
Equality deduction for restricted universal quantifier. (Contributed by
NM, 13-Nov-2005.)
|
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜓)) |
|
Theorem | rexeqdv 2693* |
Equality deduction for restricted existential quantifier. (Contributed
by NM, 14-Jan-2007.)
|
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜓)) |
|
Theorem | raleqbi1dv 2694* |
Equality deduction for restricted universal quantifier. (Contributed by
NM, 16-Nov-1995.)
|
⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜓)) |
|
Theorem | rexeqbi1dv 2695* |
Equality deduction for restricted existential quantifier. (Contributed
by NM, 18-Mar-1997.)
|
⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜓)) |
|
Theorem | reueqd 2696* |
Equality deduction for restricted unique existential quantifier.
(Contributed by NM, 5-Apr-2004.)
|
⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 = 𝐵 → (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥 ∈ 𝐵 𝜓)) |
|
Theorem | rmoeqd 2697* |
Equality deduction for restricted at-most-one quantifier. (Contributed
by Alexander van der Vekens, 17-Jun-2017.)
|
⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 = 𝐵 → (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥 ∈ 𝐵 𝜓)) |
|
Theorem | raleqbidv 2698* |
Equality deduction for restricted universal quantifier. (Contributed by
NM, 6-Nov-2007.)
|
⊢ (𝜑 → 𝐴 = 𝐵)
& ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒)) |
|
Theorem | rexeqbidv 2699* |
Equality deduction for restricted universal quantifier. (Contributed by
NM, 6-Nov-2007.)
|
⊢ (𝜑 → 𝐴 = 𝐵)
& ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜒)) |
|
Theorem | raleqbidva 2700* |
Equality deduction for restricted universal quantifier. (Contributed by
Mario Carneiro, 5-Jan-2017.)
|
⊢ (𝜑 → 𝐴 = 𝐵)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒)) |