Statement List for Metamath Proof Explorer - 1301-1400 - Page 14 of 58
| Type | Label | Description |
|---|
| Statement |
|---|
| |
| Theorem | r19.40 1301 |
Restricted quantifier version of Theorem 19.40 of [Margaris] p. 90.
|
| ⊢
(∃x ∈ A (φ ∧
ψ) → (∃x ∈ A
φ ∧ ∃x ∈ A
ψ)) |
| |
| Theorem | r19.41v 1302 |
Restricted quantifier version of Theorem 19.41 of [Margaris] p. 90.
|
| ⊢
(∃x ∈ A (φ ∧
ψ) ↔ (∃x ∈ A
φ ∧ ψ)) |
| |
| Theorem | r19.42v 1303 |
Restricted version of Theorem 19.42 of [Margaris] p. 90.
|
| ⊢
(∃x ∈ A (φ ∧
ψ) ↔ (φ ∧ ∃x ∈ A
ψ)) |
| |
| Theorem | r19.43 1304 |
Restricted version of Theorem 19.43 of [Margaris] p. 90.
|
| ⊢
(∃x ∈ A (φ ∨
ψ) ↔ (∃x ∈ A
φ ∨ ∃x ∈ A
ψ)) |
| |
| Theorem | r19.44av 1305 |
One direction of a restricted quantifier version of Theorem 19.44 of
[Margaris] p. 90. The other direction
doesn't hold when A is
empty.
|
| ⊢
(∃x ∈ A (φ ∨
ψ) → (∃x ∈ A
φ ∨ ψ)) |
| |
| Theorem | r19.45av 1306 |
Restricted version of one direction of Theorem 19.45 of [Margaris]
p. 90. (The other direction doesn't hold when A is empty.)
|
| ⊢
(∃x ∈ A (φ ∨
ψ) → (φ ∨ ∃x ∈ A
ψ)) |
| |
| Theorem | hbreu1 1307 |
x is not free in ∃!x ∈ Aφ.
|
| ⊢
(∃!x ∈ A φ →
∀x∃!x ∈ A
φ) |
| |
| Theorem | rabid 1308 |
An "identity" law of concretion for restricted abstraction. Special
case
of Definition 2.1 of [Quine] p. 16.
|
| ⊢
(x ∈ {x ∈ A∣φ}
↔ (x ∈ A ∧ φ)) |
| |
| Theorem | rabid2 1309 |
An "identity" law for restricted class abstraction.
|
| ⊢
(A = {x ∈ A∣φ}
↔ ∀x ∈ A φ) |
| |
| Theorem | hbrab1 1310 |
The abstraction variable in a restricted class abstraction isn't
free.
|
| ⊢
(y ∈ {x ∈ A∣φ}
→ ∀x y ∈ {x
∈ A∣φ}) |
| |
| Theorem | hbrab 1311 |
A variable not free in a wff remains so in a restricted class
abstraction.
|
| ⊢
(φ → ∀xφ)
& ⊢ (z ∈ A
→ ∀x z ∈ A) ⇒ ⊢ (z ∈
{y ∈ A∣φ}
→ ∀x z ∈ {y
∈ A∣φ}) |
| |
| Theorem | ralcom 1312 |
Commutation of restricted quantifiers.
|
| ⊢
(∀x ∈ A ∀y
∈ B φ ↔ ∀y ∈ B
∀x ∈ A φ) |
| |
| Theorem | rexcom 1313 |
Commutation of restricted quantifiers.
|
| ⊢
(∃x ∈ A ∃y
∈ B φ ↔ ∃y ∈ B
∃x ∈ A φ) |
| |
| Theorem | ralcom2 1314 |
Commutation of restricted quantifiers. Note that x and y
needn't be distinct (this makes the proof longer but illustrates
the use of ddelim 1000).
|
| ⊢
(∀x ∈ A ∀y
∈ A φ → ∀y ∈ A
∀x ∈ A φ) |
| |
| Theorem | ralcom3 1315 |
A commutative law for restricted quantifiers that swaps the domain
of the restriction.
|
| ⊢
(∀x ∈ A (x ∈
B → φ) ↔ ∀x ∈ B
(x ∈ A → φ)) |
| |
| Theorem | reeanv 1316 |
Rearrange existential quantifiers.
|
| ⊢
(∃x ∈ A ∃y
∈ B (φ ∧ ψ) ↔ (∃x ∈ A
φ ∧ ∃y ∈ B
ψ)) |
| |
| Theorem | bireudva 1317 |
Formula-building rule for restricted existential quantifier (deduction
rule).
|
| ⊢
((φ ∧ x ∈ A)
→ (ψ ↔ χ))
⇒ ⊢ (φ → (∃!x ∈ A
ψ ↔ ∃!x ∈ A
χ)) |
| |
| Theorem | bireudv 1318 |
Formula-building rule for restricted existential quantifier (deduction
rule).
|
| ⊢
(φ → (ψ ↔ χ))
⇒ ⊢ (φ → (∃!x ∈ A
ψ ↔ ∃!x ∈ A
χ)) |
| |
| Theorem | bireua 1319 |
Formula-building rule for restricted existential quantifier (inference
rule).
|
| ⊢
(x ∈ A → (φ
↔ ψ))
⇒ ⊢
(∃!x ∈ A φ ↔
∃!x ∈ A ψ) |
| |
| Theorem | bireu 1320 |
Formula-building rule for restricted existential quantifier (inference
rule).
|
| ⊢
(φ ↔ ψ)
⇒ ⊢
(∃!x ∈ A φ ↔
∃!x ∈ A ψ) |
| |
| Theorem | raleqf 1321 |
Equality theorem for restricted universal quantifier, with bound
variable hypotheses instead of distinct variable restrictions.
|
| ⊢
(y ∈ A → ∀x y ∈
A)
& ⊢ (y ∈ B
→ ∀x y ∈ B) ⇒ ⊢ (A =
B → (∀x ∈ A
φ ↔ ∀x ∈ B
φ)) |
| |
| Theorem | rexeqf 1322 |
Equality theorem for restricted existential quantifier, with bound
variable hypotheses instead of distinct variable restrictions.
|
| ⊢
(y ∈ A → ∀x y ∈
A)
& ⊢ (y ∈ B
→ ∀x y ∈ B) ⇒ ⊢ (A =
B → (∃x ∈ A
φ ↔ ∃x ∈ B
φ)) |
| |
| Theorem | reueqf 1323 |
Equality theorem for restricted uniqueness quantifier, with bound
variable hypotheses instead of distinct variable restrictions.
|
| ⊢
(y ∈ A → ∀x y ∈
A)
& ⊢ (y ∈ B
→ ∀x y ∈ B) ⇒ ⊢ (A =
B → (∃!x ∈ A
φ ↔ ∃!x ∈ B
φ)) |
| |
| Theorem | raleq 1324 |
Equality theorem for restricted universal quantifier.
|
| ⊢
(A = B → (∀x ∈ A
φ ↔ ∀x ∈ B
φ)) |
| |
| Theorem | rexeq 1325 |
Equality theorem for restricted existential quantifier.
|
| ⊢
(A = B → (∃x ∈ A
φ ↔ ∃x ∈ B
φ)) |
| |
| Theorem | reueq 1326 |
Equality theorem for restricted uniqueness quantifier.
|
| ⊢
(A = B → (∃!x ∈ A
φ ↔ ∃!x ∈ B
φ)) |
| |
| Theorem | raleqd 1327 |
Equality deduction for restricted universal quantifier.
|
| ⊢
(A = B → (φ
↔ ψ))
⇒ ⊢ (A = B →
(∀x ∈ A φ ↔
∀x ∈ B ψ)) |
| |
| Theorem | rexeqd 1328 |
Equality deduction for restricted existential quantifier.
|
| ⊢
(A = B → (φ
↔ ψ))
⇒ ⊢ (A = B →
(∃x ∈ A φ ↔
∃x ∈ B ψ)) |
| |
| Theorem | reueqd 1329 |
Equality deduction for restricted uniqueness quantifier.
|
| ⊢
(A = B → (φ
↔ ψ))
⇒ ⊢ (A = B →
(∃!x ∈ A φ ↔
∃!x ∈ B ψ)) |
| |
| Theorem | cbvralf 1330 |
Rule used to change bound variables with implicit substitution.
|
| ⊢
(z ∈ A → ∀x z ∈
A)
& ⊢ (z ∈ A
→ ∀y z ∈ A) & ⊢ (φ
→ ∀yφ)
& ⊢ (ψ → ∀xψ)
& ⊢ (x = y →
(φ ↔ ψ))
⇒ ⊢
(∀x ∈ A φ ↔
∀y ∈ A ψ) |
| |
| Theorem | cbvral 1331 |
Rule used to change bound variables with implicit substitution.
|
| ⊢
(φ → ∀yφ)
& ⊢ (ψ → ∀xψ)
& ⊢ (x = y →
(φ ↔ ψ))
⇒ ⊢
(∀x ∈ A φ ↔
∀y ∈ A ψ) |
| |
| Theorem | cbvrex 1332 |
Rule used to change bound variables with implicit substitution.
|
| ⊢
(φ → ∀yφ)
& ⊢ (ψ → ∀xψ)
& ⊢ (x = y →
(φ ↔ ψ))
⇒ ⊢ (∃x ∈ A
φ ↔ ∃y ∈ A
ψ) |
| |
| Theorem | cbvralv 1333 |
Change the bound variable of a restricted universal quantifier using
implicit substitution.
|
| ⊢
(x = y → (φ
↔ ψ))
⇒ ⊢
(∀x ∈ A φ ↔
∀y ∈ A ψ) |
| |
| Theorem | cbvrexv 1334 |
Change the bound variable of a restricted existential quantifier using
implicit substitution.
|
| ⊢
(x = y → (φ
↔ ψ))
⇒ ⊢ (∃x ∈ A
φ ↔ ∃y ∈ A
ψ) |
| |
| Theorem | cbvreuv 1335 |
Change the bound variable of a restricted uniqueness quantifier using
implicit substitution.
|
| ⊢
(x = y → (φ
↔ ψ))
⇒ ⊢
(∃!x ∈ A φ ↔
∃!y ∈ A ψ) |
| |
| Theorem | cbvral2v 1336 |
Change bound variables of double restricted universal quantification,
using implicit substitution.
|
| ⊢
(x = z → (φ
↔ χ))
& ⊢ (y = w →
(χ ↔ ψ))
⇒ ⊢
(∀x ∈ A ∀y
∈ B φ ↔ ∀z ∈ A
∀w ∈ B ψ) |
| |
| Theorem | reurex 1337 |
Restricted unique existence implies restricted existence.
|
| ⊢
(∃!x ∈ A φ →
∃x ∈ A φ) |
| |
| Theorem | reu2 1338 |
A way of expressing restricted uniqueness.
|
| ⊢
(∃!x ∈ A φ ↔
(∃x ∈ A φ ∧
∀x ∈ A ∀y
∈ A ((φ ∧ [y / x]φ) → x = y))) |
| |
| Theorem | reu5 1339 |
Restricted uniqueness in terms of "at most one".
|
| ⊢
(∃!x ∈ A φ ↔
(∃x ∈ A φ ∧
∃*x(x ∈ A
∧ φ))) |
| |
| Theorem | reu4 1340 |
Restricted uniqueness using implicit substitution.
|
| ⊢
(x = y → (φ
↔ ψ))
⇒ ⊢
(∃!x ∈ A φ ↔
(∃x ∈ A φ ∧
∀x ∈ A ∀y
∈ A ((φ ∧ ψ) → x = y))) |
| |
| Theorem | 2reuswap 1341 |
A condition allowing swap of uniqueness and existential quantifiers.
|
| ⊢
(∀x ∈ A ∃*y(y ∈
A ∧ φ) → (∃!x ∈ A
∃y ∈ A φ →
∃!y ∈ A ∃x
∈ A φ)) |
| |
| Theorem | birabi 1342 |
Equivalent wff's yield equal restricted class abstractions (inference
rule).
|
| ⊢
(x ∈ A → (ψ
↔ χ))
⇒ ⊢ {x ∈ A∣ψ}
= {x ∈ A∣χ} |
| |
| Theorem | birabdv 1343 |
Equivalent wff's yield equal restricted class abstractions (deduction
rule).
|
| ⊢
(φ → (x ∈ A
→ (ψ ↔ χ)))
⇒ ⊢ (φ → {x ∈ A∣ψ}
= {x ∈ A∣χ}) |
| |
| Theorem | birabsdv 1344 |
Equivalent wff's yield equal restricted class abstractions (deduction
rule).
|
| ⊢
(φ → (ψ ↔ χ))
⇒ ⊢ (φ → {x ∈ A∣ψ}
= {x ∈ A∣χ}) |
| |
| Theorem | rabeqf 1345 |
Equality theorem for restricted class abstractions, with bound variable
hypotheses instead of distinct variable restrictions.
|
| ⊢
(y ∈ A → ∀x y ∈
A)
& ⊢ (y ∈ B
→ ∀x y ∈ B) ⇒ ⊢ (A =
B → {x ∈ A∣φ}
= {x ∈ B∣φ}) |
| |
| Theorem | rabeq 1346 |
Equality theorem for restricted class abstractions.
|
| ⊢
(A = B → {x
∈ A∣φ} = {x
∈ B∣φ}) |
| |
| Theorem | cleqrabi 1347 |
Inference rule from equality of a class variable and a restricted
class abstraction.
|
| ⊢
A = {x ∈ B∣φ}
⇒ ⊢ (x ∈ A
↔ (x ∈ B ∧ φ)) |
| |
| Syntax | cvv 1348 |
Extend class notation to include the universal class symbol.
|
| class
V |
| |
| Definition | df-v 1349 |
Define the universal class. Definition 5.20 of [TakeutiZaring] p. 21.
|
| ⊢
V = {x∣x = x} |
| |
| Theorem | visset 1350 |
All set variables are sets (see isset 1351). Theorem 6.8 of [Quine]
p. 43.
|
| ⊢
x ∈ V |
| |
| Theorem | isset 1351 |
Two ways to say "A is a set": A
class A is a member of the
universal class V (see df-v 1349) if and only if the class A
exists (i.e. there exists some set x
equal to class A). Theorem
6.9 of [Quine] p. 43. Notational
convention: We will use the
notational device "A ∈
V" to mean "A is a
set" very
frequently, for example in uniex 1947. Note the when A is not a set,
it is called a proper class. In some theorems, such as uniexg 1948, in
order to shorten certain proofs we use the antecedent A ∈ B
instead
of A ∈ V to mean
"A is a set".
|
| ⊢
(A ∈ V ↔
∃x x = A) |
| |
| Theorem | isseti 1352 |
A way to say "A is a set"
(inference rule).
|
| ⊢
A ∈ V
⇒ ⊢ ∃x x = A |
| |
| Theorem | issetri 1353 |
A way to say "A is a set"
(inference rule).
|
| ⊢
∃x x = A ⇒ ⊢ A ∈
V |
| |
| Theorem | elisset 1354 |
If a class is a member of another class, it is a set. Theorem 6.12
of [Quine] p. 44.
|
| ⊢
(A ∈ B → A
∈ V) |
| |
| Theorem | elisseti 1355 |
If a class is a member of another class, it is a set.
|
| ⊢
A ∈ B ⇒ ⊢ A ∈
V |
| |
| Theorem | elex 1356 |
An element of a class exists.
|
| ⊢
(A ∈ B → ∃x x = A) |
| |
| Theorem | ralv 1357 |
A universal quantifier restricted to the universe is unrestricted.
|
| ⊢
(∀x ∈ V φ ↔ ∀xφ) |
| |
| Theorem | rexv 1358 |
An existential quantifier restricted to the universe is unrestricted.
|
| ⊢
(∃x ∈ V φ ↔ ∃xφ) |
| |
| Theorem | rabab 1359 |
A class abstraction restricted to the universe is unrestricted.
|
| ⊢
{x ∈ V∣φ} = {x∣φ} |
| |
| Theorem | ralcom4 1360 |
Commutation of restricted and unrestricted universal quantifiers.
|
| ⊢
(∀x ∈ A ∀yφ ↔
∀y∀x ∈ A
φ) |
| |
| Theorem | rexcom4 1361 |
Commutation of restricted and unrestricted existential quantifiers.
|
| ⊢
(∃x ∈ A ∃yφ ↔ ∃y∃x
∈ A φ) |
| |
| Theorem | ceqsalg 1362 |
A representation of explicit substitution of a class for a variable,
inferred from an implicit substitution hypothesis.
|
| ⊢
(ψ → ∀xψ)
& ⊢ (x = A →
(φ ↔ ψ))
⇒ ⊢ (A ∈ B
→ (∀x(x = A →
φ) ↔ ψ)) |
| |
| Theorem | ceqsal 1363 |
A representation of explicit substitution of a class for a variable,
inferred from an implicit substitution hypothesis.
|
| ⊢
(ψ → ∀xψ)
& ⊢ A ∈ V
& ⊢ (x = A →
(φ ↔ ψ))
⇒ ⊢
(∀x(x = A →
φ) ↔ ψ) |
| |
| Theorem | ceqsalv 1364 |
A representation of explicit substitution of a class for a variable,
inferred from an implicit substitution hypothesis.
|
| ⊢
A ∈ V
& ⊢ (x = A →
(φ ↔ ψ))
⇒ ⊢
(∀x(x = A →
φ) ↔ ψ) |
| |
| Theorem | gencl 1365 |
Implicit substitution for class with embedded variable.
|
| ⊢
(θ ↔ ∃x(χ ∧
A = B)) & ⊢ (A =
B → (φ ↔ ψ))
& ⊢ (χ → φ)
⇒ ⊢ (θ → ψ) |
| |
| Theorem | 2gencl 1366 |
Implicit substitution for class with embedded variable.
|
| ⊢
(C ∈ S ↔ ∃x(x ∈
R ∧ A = C)) & ⊢ (D ∈
S ↔ ∃y(y ∈
R ∧ B = D)) & ⊢ (A =
C → (φ ↔ ψ))
& ⊢ (B = D →
(ψ ↔ χ))
& ⊢ ((x ∈ R
∧ y ∈ R) → φ)
⇒ ⊢ ((C ∈ S
∧ D ∈ S) → χ) |
| |
| Theorem | 3gencl 1367 |
Implicit substitution for class with embedded variable.
|
| ⊢
(D ∈ S ↔ ∃x(x ∈
R ∧ A = D)) & ⊢ (F ∈
S ↔ ∃y(y ∈
R ∧ B = F)) & ⊢ (G ∈
S ↔ ∃z(z ∈
R ∧ C = G)) & ⊢ (A =
D → (φ ↔ ψ))
& ⊢ (B = F →
(ψ ↔ χ))
& ⊢ (C = G →
(χ ↔ θ))
& ⊢ ((x ∈ R
∧ y ∈ R ∧ z
∈ R) → φ)
⇒ ⊢ ((D ∈ S
∧ F ∈ S ∧ G
∈ S) → θ) |
| |
| Theorem | cgsex2g 1368 |
Implicit substitution inference for general classes.
|
| ⊢
((x = A ∧ y =
B) → χ)
& ⊢ (χ → (φ ↔ ψ))
⇒ ⊢ ((A ∈ C
∧ B ∈ D) → (∃x∃y(χ ∧ φ) ↔ ψ)) |
| |
| Theorem | cgsex4g 1369 |
An implicit substitution inference for 4 general classes.
|
| ⊢
(((x = A ∧ y =
B) ∧ (z = C ∧
w = D)) → χ)
& ⊢ (χ → (φ ↔ ψ))
⇒ ⊢ (((A ∈ R
∧ B ∈ S) ∧ (C
∈ R ∧ D ∈ S))
→ (∃x∃y∃z∃w(χ ∧ φ) ↔ ψ)) |
| |
| Theorem | ceqsex 1370 |
Elimination of an existential quantifier, using implicit
substitution.
|
| ⊢
(ψ → ∀xψ)
& ⊢ A ∈ V
& ⊢ (x = A →
(φ ↔ ψ))
⇒ ⊢ (∃x(x = A ∧ φ)
↔ ψ) |
| |
| Theorem | ceqsexv 1371 |
Elimination of an existential quantifier, using implicit
substitution.
|
| ⊢
A ∈ V
& ⊢ (x = A →
(φ ↔ ψ))
⇒ ⊢ (∃x(x = A ∧ φ)
↔ ψ) |
| |
| Theorem | gencbvex 1372 |
Change of bound variable using implicit substitution.
|
| ⊢
A ∈ V
& ⊢ (A = y →
(φ ↔ ψ))
& ⊢ (A = y →
(χ ↔ θ))
& ⊢ (θ ↔ ∃x(χ ∧
A = y))
⇒ ⊢ (∃x(χ ∧
φ) ↔ ∃y(θ ∧
ψ)) |
| |
| Theorem | gencbval 1373 |
Change of bound variable using implicit substitution.
|
| ⊢
A ∈ V
& ⊢ (A = y →
(φ ↔ ψ))
& ⊢ (A = y →
(χ ↔ θ))
& ⊢ (θ ↔ ∃x(χ ∧
A = y))
⇒ ⊢
(∀x(χ → φ) ↔ ∀y(θ
→ ψ)) |
| |
| Theorem | clel2 1374 |
An alternate definition of class membership when the class is a set.
|
| ⊢
A ∈ V
⇒ ⊢ (A ∈ B
↔ ∀x(x = A →
x ∈ B)) |
| |
| Theorem | clel3 1375 |
An alternate definition of class membership when the class is a set.
|
| ⊢
B ∈ V
⇒ ⊢ (A ∈ B
↔ ∃x(x = B ∧
A ∈ x)) |
| |
| Theorem | clel4 1376 |
An alternate definition of class membership when the class is a set.
|
| ⊢
B ∈ V
⇒ ⊢ (A ∈ B
↔ ∀x(x = B →
A ∈ x)) |
| |
| Theorem | vtoclf 1377 |
Implicit substitution of a class for a set variable. This is a
generalization of chv2 850.
|
| ⊢
(ψ → ∀xψ)
& ⊢ A ∈ V
& ⊢ (x = A →
(φ ↔ ψ))
& ⊢ φ
⇒ ⊢ ψ |
| |
| Theorem | vtocl 1378 |
Implicit substitution of a class for a set variable.
|
| ⊢
A ∈ V
& ⊢ (x = A →
(φ ↔ ψ))
& ⊢ φ
⇒ ⊢ ψ |
| |
| Theorem | vtocl2 1379 |
Implicit substitution of classes for set variables.
|
| ⊢
A ∈ V
& ⊢ B ∈ V
& ⊢ ((x = A ∧
y = B)
→ (φ ↔ ψ))
& ⊢ φ
⇒ ⊢ ψ |
| |
| Theorem | vtocl3 1380 |
Implicit substitution of classes for set variables.
|
| ⊢
A ∈ V
& ⊢ B ∈ V
& ⊢ C ∈ V
& ⊢ ((x = A ∧
y = B
∧ z = C) → (φ ↔ ψ))
& ⊢ φ
⇒ ⊢ ψ |
| |
| Theorem | vtoclb 1381 |
Implicit substitution of a class for a set variable.
|
| ⊢
A ∈ V
& ⊢ (x = A →
(φ ↔ χ))
& ⊢ (x = A →
(ψ ↔ θ))
& ⊢ (φ ↔ ψ)
⇒ ⊢ (χ ↔ θ) |
| |
| Theorem | vtoclgf 1382 |
Implicit substitution of a class for a set variable, with bound variable
hypotheses in place of distinct variable restrictions.
|
| ⊢
(y ∈ A → ∀x y ∈
A)
& ⊢ (ψ → ∀xψ)
& ⊢ (x = A →
(φ ↔ ψ))
& ⊢ φ
⇒ ⊢ (A ∈ B
→ ψ) |
| |
| Theorem | vtoclg 1383 |
Implicit substitution of a class for a set variable.
|
| ⊢
(x = A → (φ
↔ ψ))
& ⊢ φ
⇒ ⊢ (A ∈ B
→ ψ) |
| |
| Theorem | vtoclbg 1384 |
Implicit substitution of a class for a set variable.
|
| ⊢
(x = A → (φ
↔ χ))
& ⊢ (x = A →
(ψ ↔ θ))
& ⊢ (φ ↔ ψ)
⇒ ⊢ (A ∈ B
→ (χ ↔ θ)) |
| |
| Theorem | vtocl2gf 1385 |
Implicit substitution of a class for a set variable.
|
| ⊢
(ψ → ∀xψ)
& ⊢ (χ → ∀yχ)
& ⊢ (x = A →
(φ ↔ ψ))
& ⊢ (y = B →
(ψ ↔ χ))
& ⊢ φ
⇒ ⊢ ((A ∈ C
∧ B ∈ D) → χ) |
| |
| Theorem | vtocl2g 1386 |
Implicit substitution of 2 classes for 2 set variables.
|
| ⊢
(x = A → (φ
↔ ψ))
& ⊢ (y = B →
(ψ ↔ χ))
& ⊢ φ
⇒ ⊢ ((A ∈ C
∧ B ∈ D) → χ) |
| |
| Theorem | vtoclga 1387 |
Implicit substitution of a class for a set variable.
|
| ⊢
(x = A → (φ
↔ ψ))
& ⊢ (x ∈ B
→ φ)
⇒ ⊢ (A ∈ B
→ ψ) |
| |
| Theorem | vtocl2ga 1388 |
Implicit substitution of 2 classes for 2 set variables.
|
| ⊢
(x = A → (φ
↔ ψ))
& ⊢ (y = B →
(ψ ↔ χ))
& ⊢ ((x ∈ C
∧ y ∈ D) → φ)
⇒ ⊢ ((A ∈ C
∧ B ∈ D) → χ) |
| |
| Theorem | vtocl3ga 1389 |
Implicit substitution of 3 classes for 3 set variables.
|
| ⊢
(x = A → (φ
↔ ψ))
& ⊢ (y = B →
(ψ ↔ χ))
& ⊢ (z = C →
(χ ↔ θ))
& ⊢ ((x ∈ D
∧ y ∈ R ∧ z
∈ S) → φ)
⇒ ⊢ ((A ∈ D
∧ B ∈ R ∧ C
∈ S) → θ) |
| |
| Theorem | vtocleg 1390 |
Implicit substitution of a class for a set variable.
|
| ⊢
(x = A → φ)
⇒ ⊢ (A ∈ B
→ φ) |
| |
| Theorem | vtocle 1391 |
Implicit substitution of a class for a set variable.
|
| ⊢
A ∈ V
& ⊢ (x = A →
φ)
⇒ ⊢ φ |
| |
| Theorem | vtoclef 1392 |
Implicit substitution of a class for a set variable.
|
| ⊢
(φ → ∀xφ)
& ⊢ A ∈ V
& ⊢ (x = A →
φ)
⇒ ⊢ φ |
| |
| Theorem | vtoclri 1393 |
Implicit substitution of a class for a set variable.
|
| ⊢
(x = A → (φ
↔ ψ))
& ⊢ ∀x ∈ B
φ
⇒ ⊢ (A ∈ B
→ ψ) |
| |
| Theorem | cla4gf 1394 |
Rule of specialization with implicit substitution. Compare Theorem 7.3
of [Quine] p. 44.
|
| ⊢
(y ∈ A → ∀x y ∈
A)
& ⊢ (ψ → ∀xψ)
& ⊢ (x = A →
(φ ↔ ψ))
⇒ ⊢ (A ∈ B
→ (∀xφ → ψ)) |
| |
| Theorem | cla4egf 1395 |
Existential specialization with implicit substitution.
|
| ⊢
(y ∈ A → ∀x y ∈
A)
& ⊢ (ψ → ∀xψ)
& ⊢ (x = A →
(φ ↔ ψ))
⇒ ⊢ (A ∈ B
→ (ψ → ∃xφ)) |
| |
| Theorem | cla4gv 1396 |
Rule of specialization with implicit substitution. Compare Theorem 7.3
of [Quine] p. 44.
|
| ⊢
(x = A → (φ
↔ ψ))
⇒ ⊢ (A ∈ B
→ (∀xφ → ψ)) |
| |
| Theorem | cla4egv 1397 |
Existential specialization with implicit substitution.
|
| ⊢
(x = A → (φ
↔ ψ))
⇒ ⊢ (A ∈ B
→ (ψ → ∃xφ)) |
| |
| Theorem | cla4e2gv 1398 |
Existential specialization with 2 quantifiers, using implicit
substitution.
|
| ⊢
((x = A ∧ y =
B) → (φ ↔ ψ))
⇒ ⊢ ((A ∈ C
∧ B ∈ D) → (ψ → ∃x∃yφ)) |
| |
| Theorem | cla42gv 1399 |
Specialization with 2 quantifiers, using implicit substitution.
|
| ⊢
((x = A ∧ y =
B) → (φ ↔ ψ))
⇒ ⊢ ((A ∈ C
∧ B ∈ D) → (∀x∀yφ → ψ)) |
| |
| Theorem | cla4v 1400 |
Rule of specialization with implicit substitution.
|
| ⊢
A ∈ V
& ⊢ (x = A →
(φ ↔ ψ))
⇒ ⊢
(∀xφ → ψ) |
Home
Hilbert Space Explorer
(4958-5787)