Theorem List for Intuitionistic Logic Explorer - 2501-2600 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | r19.32r 2501 |
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.32vr 2502* |
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 2503. (Contributed by Jim Kingdon, 19-Aug-2018.)
|
⊢ ((𝜑 ∨ ∀𝑥 ∈ 𝐴 𝜓) → ∀𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓)) |
|
Theorem | r19.32vdc 2503* |
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 2504 |
Restricted quantifier version of 19.35-1 1555. (Contributed by Jim Kingdon,
4-Jun-2018.)
|
⊢ (∃𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓)) |
|
Theorem | r19.36av 2505* |
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 2506 |
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 2507* |
Restricted version of one direction of Theorem 19.37 of [Margaris]
p. 90. (Contributed by NM, 2-Apr-2004.)
|
⊢ (∃𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (𝜑 → ∃𝑥 ∈ 𝐴 𝜓)) |
|
Theorem | r19.40 2508 |
Restricted quantifier version of Theorem 19.40 of [Margaris] p. 90.
(Contributed by NM, 2-Apr-2004.)
|
⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓)) |
|
Theorem | r19.41 2509 |
Restricted quantifier version of Theorem 19.41 of [Margaris] p. 90.
(Contributed by NM, 1-Nov-2010.)
|
⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ 𝜓)) |
|
Theorem | r19.41v 2510* |
Restricted quantifier version of Theorem 19.41 of [Margaris] p. 90.
(Contributed by NM, 17-Dec-2003.)
|
⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ 𝜓)) |
|
Theorem | r19.42v 2511* |
Restricted version of Theorem 19.42 of [Margaris] p. 90. (Contributed
by NM, 27-May-1998.)
|
⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓)) |
|
Theorem | r19.43 2512 |
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 2513* |
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 2514* |
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 2515* |
Commutation of restricted quantifiers. (Contributed by Mario Carneiro,
14-Oct-2016.)
|
⊢ Ⅎ𝑦𝐴
& ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 𝜑) |
|
Theorem | rexcomf 2516* |
Commutation of restricted quantifiers. (Contributed by Mario Carneiro,
14-Oct-2016.)
|
⊢ Ⅎ𝑦𝐴
& ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) |
|
Theorem | ralcom 2517* |
Commutation of restricted quantifiers. (Contributed by NM,
13-Oct-1999.) (Revised by Mario Carneiro, 14-Oct-2016.)
|
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 𝜑) |
|
Theorem | rexcom 2518* |
Commutation of restricted quantifiers. (Contributed by NM,
19-Nov-1995.) (Revised by Mario Carneiro, 14-Oct-2016.)
|
⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) |
|
Theorem | rexcom13 2519* |
Swap 1st and 3rd restricted existential quantifiers. (Contributed by
NM, 8-Apr-2015.)
|
⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐶 𝜑 ↔ ∃𝑧 ∈ 𝐶 ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) |
|
Theorem | rexrot4 2520* |
Rotate existential restricted quantifiers twice. (Contributed by NM,
8-Apr-2015.)
|
⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐶 ∃𝑤 ∈ 𝐷 𝜑 ↔ ∃𝑧 ∈ 𝐶 ∃𝑤 ∈ 𝐷 ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) |
|
Theorem | ralcom3 2521 |
A commutative law for restricted quantifiers that swaps the domain of the
restriction. (Contributed by NM, 22-Feb-2004.)
|
⊢ (∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝐵 → 𝜑) ↔ ∀𝑥 ∈ 𝐵 (𝑥 ∈ 𝐴 → 𝜑)) |
|
Theorem | reean 2522* |
Rearrange existential quantifiers. (Contributed by NM, 27-Oct-2010.)
(Proof shortened by Andrew Salmon, 30-May-2011.)
|
⊢ Ⅎ𝑦𝜑
& ⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐵 𝜓)) |
|
Theorem | reeanv 2523* |
Rearrange existential quantifiers. (Contributed by NM, 9-May-1999.)
|
⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐵 𝜓)) |
|
Theorem | 3reeanv 2524* |
Rearrange three existential quantifiers. (Contributed by Jeff Madsen,
11-Jun-2010.)
|
⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐶 (𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐵 𝜓 ∧ ∃𝑧 ∈ 𝐶 𝜒)) |
|
Theorem | nfreu1 2525 |
𝑥
is not free in ∃!𝑥 ∈ 𝐴𝜑. (Contributed by NM,
19-Mar-1997.)
|
⊢ Ⅎ𝑥∃!𝑥 ∈ 𝐴 𝜑 |
|
Theorem | nfrmo1 2526 |
𝑥
is not free in ∃*𝑥 ∈ 𝐴𝜑. (Contributed by NM,
16-Jun-2017.)
|
⊢ Ⅎ𝑥∃*𝑥 ∈ 𝐴 𝜑 |
|
Theorem | nfreudxy 2527* |
Not-free deduction for restricted uniqueness. This is a version where
𝑥 and 𝑦 are distinct.
(Contributed by Jim Kingdon,
6-Jun-2018.)
|
⊢ Ⅎ𝑦𝜑
& ⊢ (𝜑 → Ⅎ𝑥𝐴)
& ⊢ (𝜑 → Ⅎ𝑥𝜓) ⇒ ⊢ (𝜑 → Ⅎ𝑥∃!𝑦 ∈ 𝐴 𝜓) |
|
Theorem | nfreuxy 2528* |
Not-free for restricted uniqueness. This is a version where 𝑥 and
𝑦 are distinct. (Contributed by Jim
Kingdon, 6-Jun-2018.)
|
⊢ Ⅎ𝑥𝐴
& ⊢ Ⅎ𝑥𝜑 ⇒ ⊢ Ⅎ𝑥∃!𝑦 ∈ 𝐴 𝜑 |
|
Theorem | rabid 2529 |
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 2530* |
An "identity" law for restricted class abstraction. (Contributed by
NM,
9-Oct-2003.) (Proof shortened by Andrew Salmon, 30-May-2011.)
|
⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ ∀𝑥 ∈ 𝐴 𝜑) |
|
Theorem | rabbi 2531 |
Equivalent wff's correspond to equal restricted class abstractions.
Closed theorem form of rabbidva 2592. (Contributed by NM, 25-Nov-2013.)
|
⊢ (∀𝑥 ∈ 𝐴 (𝜓 ↔ 𝜒) ↔ {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒}) |
|
Theorem | rabswap 2532 |
Swap with a membership relation in a restricted class abstraction.
(Contributed by NM, 4-Jul-2005.)
|
⊢ {𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝐵} = {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝐴} |
|
Theorem | nfrab1 2533 |
The abstraction variable in a restricted class abstraction isn't free.
(Contributed by NM, 19-Mar-1997.)
|
⊢ Ⅎ𝑥{𝑥 ∈ 𝐴 ∣ 𝜑} |
|
Theorem | nfrabxy 2534* |
A variable not free in a wff remains so in a restricted class
abstraction. (Contributed by Jim Kingdon, 19-Jul-2018.)
|
⊢ Ⅎ𝑥𝜑
& ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥{𝑦 ∈ 𝐴 ∣ 𝜑} |
|
Theorem | reubida 2535 |
Formula-building rule for restricted existential quantifier (deduction
rule). (Contributed by Mario Carneiro, 19-Nov-2016.)
|
⊢ Ⅎ𝑥𝜑
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐴 𝜒)) |
|
Theorem | reubidva 2536* |
Formula-building rule for restricted existential quantifier (deduction
rule). (Contributed by NM, 13-Nov-2004.)
|
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐴 𝜒)) |
|
Theorem | reubidv 2537* |
Formula-building rule for restricted existential quantifier (deduction
rule). (Contributed by NM, 17-Oct-1996.)
|
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐴 𝜒)) |
|
Theorem | reubiia 2538 |
Formula-building rule for restricted existential quantifier (inference
rule). (Contributed by NM, 14-Nov-2004.)
|
⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥 ∈ 𝐴 𝜓) |
|
Theorem | reubii 2539 |
Formula-building rule for restricted existential quantifier (inference
rule). (Contributed by NM, 22-Oct-1999.)
|
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥 ∈ 𝐴 𝜓) |
|
Theorem | rmobida 2540 |
Formula-building rule for restricted existential quantifier (deduction
rule). (Contributed by NM, 16-Jun-2017.)
|
⊢ Ⅎ𝑥𝜑
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃*𝑥 ∈ 𝐴 𝜓 ↔ ∃*𝑥 ∈ 𝐴 𝜒)) |
|
Theorem | rmobidva 2541* |
Formula-building rule for restricted existential quantifier (deduction
rule). (Contributed by NM, 16-Jun-2017.)
|
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃*𝑥 ∈ 𝐴 𝜓 ↔ ∃*𝑥 ∈ 𝐴 𝜒)) |
|
Theorem | rmobidv 2542* |
Formula-building rule for restricted existential quantifier (deduction
rule). (Contributed by NM, 16-Jun-2017.)
|
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃*𝑥 ∈ 𝐴 𝜓 ↔ ∃*𝑥 ∈ 𝐴 𝜒)) |
|
Theorem | rmobiia 2543 |
Formula-building rule for restricted existential quantifier (inference
rule). (Contributed by NM, 16-Jun-2017.)
|
⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥 ∈ 𝐴 𝜓) |
|
Theorem | rmobii 2544 |
Formula-building rule for restricted existential quantifier (inference
rule). (Contributed by NM, 16-Jun-2017.)
|
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥 ∈ 𝐴 𝜓) |
|
Theorem | raleqf 2545 |
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 2546 |
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 2547 |
Equality theorem for restricted uniqueness 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 2548 |
Equality theorem for restricted uniqueness quantifier, with
bound-variable hypotheses instead of distinct variable restrictions.
(Contributed by Alexander van der Vekens, 17-Jun-2017.)
|
⊢ Ⅎ𝑥𝐴
& ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (𝐴 = 𝐵 → (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥 ∈ 𝐵 𝜑)) |
|
Theorem | raleq 2549* |
Equality theorem for restricted universal quantifier. (Contributed by
NM, 16-Nov-1995.)
|
⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑)) |
|
Theorem | rexeq 2550* |
Equality theorem for restricted existential quantifier. (Contributed by
NM, 29-Oct-1995.)
|
⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜑)) |
|
Theorem | reueq1 2551* |
Equality theorem for restricted uniqueness quantifier. (Contributed by
NM, 5-Apr-2004.)
|
⊢ (𝐴 = 𝐵 → (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥 ∈ 𝐵 𝜑)) |
|
Theorem | rmoeq1 2552* |
Equality theorem for restricted uniqueness quantifier. (Contributed by
Alexander van der Vekens, 17-Jun-2017.)
|
⊢ (𝐴 = 𝐵 → (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥 ∈ 𝐵 𝜑)) |
|
Theorem | raleqi 2553* |
Equality inference for restricted universal qualifier. (Contributed by
Paul Chapman, 22-Jun-2011.)
|
⊢ 𝐴 = 𝐵 ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑) |
|
Theorem | rexeqi 2554* |
Equality inference for restricted existential qualifier. (Contributed
by Mario Carneiro, 23-Apr-2015.)
|
⊢ 𝐴 = 𝐵 ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜑) |
|
Theorem | raleqdv 2555* |
Equality deduction for restricted universal quantifier. (Contributed by
NM, 13-Nov-2005.)
|
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜓)) |
|
Theorem | rexeqdv 2556* |
Equality deduction for restricted existential quantifier. (Contributed
by NM, 14-Jan-2007.)
|
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜓)) |
|
Theorem | raleqbi1dv 2557* |
Equality deduction for restricted universal quantifier. (Contributed by
NM, 16-Nov-1995.)
|
⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜓)) |
|
Theorem | rexeqbi1dv 2558* |
Equality deduction for restricted existential quantifier. (Contributed
by NM, 18-Mar-1997.)
|
⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜓)) |
|
Theorem | reueqd 2559* |
Equality deduction for restricted uniqueness quantifier. (Contributed
by NM, 5-Apr-2004.)
|
⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 = 𝐵 → (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥 ∈ 𝐵 𝜓)) |
|
Theorem | rmoeqd 2560* |
Equality deduction for restricted uniqueness quantifier. (Contributed
by Alexander van der Vekens, 17-Jun-2017.)
|
⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 = 𝐵 → (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥 ∈ 𝐵 𝜓)) |
|
Theorem | raleqbidv 2561* |
Equality deduction for restricted universal quantifier. (Contributed by
NM, 6-Nov-2007.)
|
⊢ (𝜑 → 𝐴 = 𝐵)
& ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒)) |
|
Theorem | rexeqbidv 2562* |
Equality deduction for restricted universal quantifier. (Contributed by
NM, 6-Nov-2007.)
|
⊢ (𝜑 → 𝐴 = 𝐵)
& ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜒)) |
|
Theorem | raleqbidva 2563* |
Equality deduction for restricted universal quantifier. (Contributed by
Mario Carneiro, 5-Jan-2017.)
|
⊢ (𝜑 → 𝐴 = 𝐵)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒)) |
|
Theorem | rexeqbidva 2564* |
Equality deduction for restricted universal quantifier. (Contributed by
Mario Carneiro, 5-Jan-2017.)
|
⊢ (𝜑 → 𝐴 = 𝐵)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜒)) |
|
Theorem | mormo 2565 |
Unrestricted "at most one" implies restricted "at most
one". (Contributed
by NM, 16-Jun-2017.)
|
⊢ (∃*𝑥𝜑 → ∃*𝑥 ∈ 𝐴 𝜑) |
|
Theorem | reu5 2566 |
Restricted uniqueness in terms of "at most one." (Contributed by NM,
23-May-1999.) (Revised by NM, 16-Jun-2017.)
|
⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐴 𝜑)) |
|
Theorem | reurex 2567 |
Restricted unique existence implies restricted existence. (Contributed by
NM, 19-Aug-1999.)
|
⊢ (∃!𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜑) |
|
Theorem | reurmo 2568 |
Restricted existential uniqueness implies restricted "at most one."
(Contributed by NM, 16-Jun-2017.)
|
⊢ (∃!𝑥 ∈ 𝐴 𝜑 → ∃*𝑥 ∈ 𝐴 𝜑) |
|
Theorem | rmo5 2569 |
Restricted "at most one" in term of uniqueness. (Contributed by NM,
16-Jun-2017.)
|
⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 → ∃!𝑥 ∈ 𝐴 𝜑)) |
|
Theorem | nrexrmo 2570 |
Nonexistence implies restricted "at most one". (Contributed by NM,
17-Jun-2017.)
|
⊢ (¬ ∃𝑥 ∈ 𝐴 𝜑 → ∃*𝑥 ∈ 𝐴 𝜑) |
|
Theorem | cbvralf 2571 |
Rule used to change bound variables, using implicit substitution.
(Contributed by NM, 7-Mar-2004.) (Revised by Mario Carneiro,
9-Oct-2016.)
|
⊢ Ⅎ𝑥𝐴
& ⊢ Ⅎ𝑦𝐴
& ⊢ Ⅎ𝑦𝜑
& ⊢ Ⅎ𝑥𝜓
& ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓) |
|
Theorem | cbvrexf 2572 |
Rule used to change bound variables, using implicit substitution.
(Contributed by FL, 27-Apr-2008.) (Revised by Mario Carneiro,
9-Oct-2016.) (Proof rewritten by Jim Kingdon, 10-Jun-2018.)
|
⊢ Ⅎ𝑥𝐴
& ⊢ Ⅎ𝑦𝐴
& ⊢ Ⅎ𝑦𝜑
& ⊢ Ⅎ𝑥𝜓
& ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓) |
|
Theorem | cbvral 2573* |
Rule used to change bound variables, using implicit substitution.
(Contributed by NM, 31-Jul-2003.)
|
⊢ Ⅎ𝑦𝜑
& ⊢ Ⅎ𝑥𝜓
& ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓) |
|
Theorem | cbvrex 2574* |
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 2575* |
Change the bound variable of a restricted uniqueness quantifier using
implicit substitution. (Contributed by Mario Carneiro, 15-Oct-2016.)
|
⊢ Ⅎ𝑦𝜑
& ⊢ Ⅎ𝑥𝜓
& ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑦 ∈ 𝐴 𝜓) |
|
Theorem | cbvrmo 2576* |
Change the bound variable of restricted "at most one" using implicit
substitution. (Contributed by NM, 16-Jun-2017.)
|
⊢ Ⅎ𝑦𝜑
& ⊢ Ⅎ𝑥𝜓
& ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑦 ∈ 𝐴 𝜓) |
|
Theorem | cbvralv 2577* |
Change the bound variable of a restricted universal quantifier using
implicit substitution. (Contributed by NM, 28-Jan-1997.)
|
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓) |
|
Theorem | cbvrexv 2578* |
Change the bound variable of a restricted existential quantifier using
implicit substitution. (Contributed by NM, 2-Jun-1998.)
|
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓) |
|
Theorem | cbvreuv 2579* |
Change the bound variable of a restricted uniqueness quantifier using
implicit substitution. (Contributed by NM, 5-Apr-2004.) (Revised by
Mario Carneiro, 15-Oct-2016.)
|
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑦 ∈ 𝐴 𝜓) |
|
Theorem | cbvrmov 2580* |
Change the bound variable of a restricted uniqueness quantifier using
implicit substitution. (Contributed by Alexander van der Vekens,
17-Jun-2017.)
|
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑦 ∈ 𝐴 𝜓) |
|
Theorem | cbvraldva2 2581* |
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 2582* |
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 2583* |
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 2584* |
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 | cbvral2v 2585* |
Change bound variables of double restricted universal quantification,
using implicit substitution. (Contributed by NM, 10-Aug-2004.)
|
⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜒)) & ⊢ (𝑦 = 𝑤 → (𝜒 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐵 𝜓) |
|
Theorem | cbvrex2v 2586* |
Change bound variables of double restricted universal quantification,
using implicit substitution. (Contributed by FL, 2-Jul-2012.)
|
⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜒)) & ⊢ (𝑦 = 𝑤 → (𝜒 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝜓) |
|
Theorem | cbvral3v 2587* |
Change bound variables of triple restricted universal quantification,
using implicit substitution. (Contributed by NM, 10-May-2005.)
|
⊢ (𝑥 = 𝑤 → (𝜑 ↔ 𝜒)) & ⊢ (𝑦 = 𝑣 → (𝜒 ↔ 𝜃)) & ⊢ (𝑧 = 𝑢 → (𝜃 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜑 ↔ ∀𝑤 ∈ 𝐴 ∀𝑣 ∈ 𝐵 ∀𝑢 ∈ 𝐶 𝜓) |
|
Theorem | cbvralsv 2588* |
Change bound variable by using a substitution. (Contributed by NM,
20-Nov-2005.) (Revised by Andrew Salmon, 11-Jul-2011.)
|
⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 [𝑦 / 𝑥]𝜑) |
|
Theorem | cbvrexsv 2589* |
Change bound variable by using a substitution. (Contributed by NM,
2-Mar-2008.) (Revised by Andrew Salmon, 11-Jul-2011.)
|
⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 [𝑦 / 𝑥]𝜑) |
|
Theorem | sbralie 2590* |
Implicit to explicit substitution that swaps variables in a quantified
expression. (Contributed by NM, 5-Sep-2004.)
|
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ([𝑥 / 𝑦]∀𝑥 ∈ 𝑦 𝜑 ↔ ∀𝑦 ∈ 𝑥 𝜓) |
|
Theorem | rabbiia 2591 |
Equivalent wff's yield equal restricted class abstractions (inference
rule). (Contributed by NM, 22-May-1999.)
|
⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐴 ∣ 𝜓} |
|
Theorem | rabbidva 2592* |
Equivalent wff's yield equal restricted class abstractions (deduction
rule). (Contributed by NM, 28-Nov-2003.)
|
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒}) |
|
Theorem | rabbidv 2593* |
Equivalent wff's yield equal restricted class abstractions (deduction
rule). (Contributed by NM, 10-Feb-1995.)
|
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒}) |
|
Theorem | rabeqf 2594 |
Equality theorem for restricted class abstractions, with bound-variable
hypotheses instead of distinct variable restrictions. (Contributed by
NM, 7-Mar-2004.)
|
⊢ Ⅎ𝑥𝐴
& ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜑}) |
|
Theorem | rabeq 2595* |
Equality theorem for restricted class abstractions. (Contributed by NM,
15-Oct-2003.)
|
⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜑}) |
|
Theorem | rabeqbidv 2596* |
Equality of restricted class abstractions. (Contributed by Jeff Madsen,
1-Dec-2009.)
|
⊢ (𝜑 → 𝐴 = 𝐵)
& ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒}) |
|
Theorem | rabeqbidva 2597* |
Equality of restricted class abstractions. (Contributed by Mario
Carneiro, 26-Jan-2017.)
|
⊢ (𝜑 → 𝐴 = 𝐵)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒}) |
|
Theorem | rabeq2i 2598 |
Inference rule from equality of a class variable and a restricted class
abstraction. (Contributed by NM, 16-Feb-2004.)
|
⊢ 𝐴 = {𝑥 ∈ 𝐵 ∣ 𝜑} ⇒ ⊢ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐵 ∧ 𝜑)) |
|
Theorem | cbvrab 2599 |
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 2600* |
Rule to change the bound variable in a restricted class abstraction,
using implicit substitution. (Contributed by NM, 26-May-1999.)
|
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐴 ∣ 𝜓} |