P. 450 of Theorem List - Metamath Proof Explorer

Home	Metamath Proof Explorer Theorem List (p. 450 of 498)	< 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:

Metamath Proof Explorer
(1-30854)

Hilbert Space Explorer
(30855-32377)

Users' Mathboxes
(32378-49798)

Theorem List for Metamath Proof Explorer - 44901-45000 *Has distinct variable group(s)

Type

Label

Description

Statement

Theorem

hbalgVD 44901

Virtual deduction proof of hbalg 44552. The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. hbalg 44552 is hbalgVD 44901 without virtual deductions and was automatically derived from hbalgVD 44901. (Contributed by Alan Sare, 8-Feb-2014.) (Proof modification is discouraged.) (New usage is discouraged.)

1::	⊢ ( ∀𝑦(𝜑 → ∀𝑥𝜑) ▶ ∀𝑦(𝜑 → ∀𝑥𝜑) )
2:1:	⊢ ( ∀𝑦(𝜑 → ∀𝑥𝜑) ▶ (∀𝑦𝜑 → ∀𝑦∀𝑥𝜑) )
3::	⊢ (∀𝑦∀𝑥𝜑 → ∀𝑥∀𝑦𝜑)
4:2,3:	⊢ ( ∀𝑦(𝜑 → ∀𝑥𝜑) ▶ (∀𝑦𝜑 → ∀𝑥∀𝑦𝜑) )
5::	⊢ (∀𝑦(𝜑 → ∀𝑥𝜑) → ∀𝑦∀𝑦( 𝜑 → ∀𝑥𝜑))
6:5,4:	⊢ ( ∀𝑦(𝜑 → ∀𝑥𝜑) ▶ ∀𝑦(∀ 𝑦𝜑 → ∀𝑥∀𝑦𝜑) )
qed:6:	⊢ (∀𝑦(𝜑 → ∀𝑥𝜑) → ∀𝑦(∀𝑦 𝜑 → ∀𝑥∀𝑦𝜑))

(∀𝑦(𝜑 → ∀𝑥𝜑) → ∀𝑦(∀𝑦𝜑 → ∀𝑥∀𝑦𝜑))

Theorem

hbexgVD 44902

Virtual deduction proof of hbexg 44553. The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. hbexg 44553 is hbexgVD 44902 without virtual deductions and was automatically derived from hbexgVD 44902. (Contributed by Alan Sare, 8-Feb-2014.) (Proof modification is discouraged.) (New usage is discouraged.)

1::	⊢ ( ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑) ▶ ∀𝑥 ∀𝑦(𝜑 → ∀𝑥𝜑) )
2:1:	⊢ ( ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑) ▶ ∀𝑦 ∀𝑥(𝜑 → ∀𝑥𝜑) )
3:2:	⊢ ( ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑) ▶ ∀𝑥 (𝜑 → ∀𝑥𝜑) )
4:3:	⊢ ( ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑) ▶ ∀𝑥 (¬ 𝜑 → ∀𝑥¬ 𝜑) )
5::	⊢ (∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑) ↔ ∀𝑦 ∀𝑥(𝜑 → ∀𝑥𝜑))
6::	⊢ (∀𝑦∀𝑥(𝜑 → ∀𝑥𝜑) → ∀𝑦 ∀𝑦∀𝑥(𝜑 → ∀𝑥𝜑))
7:5:	⊢ (∀𝑦∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑) ↔ ∀𝑦∀𝑦∀𝑥(𝜑 → ∀𝑥𝜑))
8:5,6,7:	⊢ (∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑) → ∀𝑦 ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑))
9:8,4:	⊢ ( ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑) ▶ ∀𝑦 ∀𝑥(¬ 𝜑 → ∀𝑥¬ 𝜑) )
10:9:	⊢ ( ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑) ▶ ∀𝑥 ∀𝑦(¬ 𝜑 → ∀𝑥¬ 𝜑) )
11:10:	⊢ ( ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑) ▶ ∀𝑦 (¬ 𝜑 → ∀𝑥¬ 𝜑) )
12:11:	⊢ ( ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑) ▶ ∀𝑦 (∀𝑦¬ 𝜑 → ∀𝑥∀𝑦¬ 𝜑) )
13:12:	⊢ ( ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑) ▶ (∀ 𝑦¬ 𝜑 → ∀𝑥∀𝑦¬ 𝜑) )
14::	⊢ (∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑) → ∀𝑥 ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑))
15:13,14:	⊢ ( ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑) ▶ ∀𝑥 (∀𝑦¬ 𝜑 → ∀𝑥∀𝑦¬ 𝜑) )
16:15:	⊢ ( ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑) ▶ ∀𝑥 (¬ ∀𝑦¬ 𝜑 → ∀𝑥¬ ∀𝑦¬ 𝜑) )
17:16:	⊢ ( ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑) ▶ (¬ ∀𝑦¬ 𝜑 → ∀𝑥¬ ∀𝑦¬ 𝜑) )
18::	⊢ (∃𝑦𝜑 ↔ ¬ ∀𝑦¬ 𝜑)
19:17,18:	⊢ ( ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑) ▶ (∃ 𝑦𝜑 → ∀𝑥¬ ∀𝑦¬ 𝜑) )
20:18:	⊢ (∀𝑥∃𝑦𝜑 ↔ ∀𝑥¬ ∀𝑦¬ 𝜑)
21:19,20:	⊢ ( ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑) ▶ (∃ 𝑦𝜑 → ∀𝑥∃𝑦𝜑) )
22:8,21:	⊢ ( ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑) ▶ ∀𝑦 (∃𝑦𝜑 → ∀𝑥∃𝑦𝜑) )
23:14,22:	⊢ ( ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑) ▶ ∀𝑥 ∀𝑦(∃𝑦𝜑 → ∀𝑥∃𝑦𝜑) )
qed:23:	⊢ ( ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑) ▶ ∀𝑥 ∀𝑦(∃𝑦𝜑 → ∀𝑥∃𝑦𝜑) )

(∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑) → ∀𝑥∀𝑦(∃𝑦𝜑 → ∀𝑥∃𝑦𝜑))

Theorem

ax6e2eqVD 44903*

The following User's Proof is a Virtual Deduction proof (see wvd1 44566) completed automatically by a Metamath tools program invoking mmj2 and the Metamath Proof Assistant. ax6e2eq 44554 is ax6e2eqVD 44903 without virtual deductions and was automatically derived from ax6e2eqVD 44903. (Contributed by Alan Sare, 25-Mar-2014.) (Proof modification is discouraged.) (New usage is discouraged.)

1::	⊢ ( ∀𝑥𝑥 = 𝑦 ▶ ∀𝑥𝑥 = 𝑦 )
2::	⊢ ( ∀𝑥𝑥 = 𝑦 , 𝑥 = 𝑢 ▶ 𝑥 = 𝑢 )
3:1:	⊢ ( ∀𝑥𝑥 = 𝑦 ▶ 𝑥 = 𝑦 )
4:2,3:	⊢ ( ∀𝑥𝑥 = 𝑦 , 𝑥 = 𝑢 ▶ 𝑦 = 𝑢 )
5:2,4:	⊢ ( ∀𝑥𝑥 = 𝑦 , 𝑥 = 𝑢 ▶ (𝑥 = 𝑢 ∧ 𝑦 = 𝑢) )
6:5:	⊢ ( ∀𝑥𝑥 = 𝑦 ▶ (𝑥 = 𝑢 → (𝑥 = 𝑢 ∧ 𝑦 = 𝑢)) )
7:6:	⊢ (∀𝑥𝑥 = 𝑦 → (𝑥 = 𝑢 → (𝑥 = 𝑢 ∧ 𝑦 = 𝑢)))
8:7:	⊢ (∀𝑥∀𝑥𝑥 = 𝑦 → ∀𝑥(𝑥 = 𝑢 → ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢)))
9::	⊢ (∀𝑥𝑥 = 𝑦 ↔ ∀𝑥∀𝑥𝑥 = 𝑦)
10:8,9:	⊢ (∀𝑥𝑥 = 𝑦 → ∀𝑥(𝑥 = 𝑢 → (𝑥 = 𝑢 ∧ 𝑦 = 𝑢)))
11:1,10:	⊢ ( ∀𝑥𝑥 = 𝑦 ▶ ∀𝑥(𝑥 = 𝑢 → (𝑥 = 𝑢 ∧ 𝑦 = 𝑢)) )
12:11:	⊢ ( ∀𝑥𝑥 = 𝑦 ▶ (∃𝑥𝑥 = 𝑢 → ∃𝑥 (𝑥 = 𝑢 ∧ 𝑦 = 𝑢)) )
13::	⊢ ∃𝑥𝑥 = 𝑢
14:13,12:	⊢ ( ∀𝑥𝑥 = 𝑦 ▶ ∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑢 ) )
140:14:	⊢ (∀𝑥𝑥 = 𝑦 → ∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑢) )
141:140:	⊢ (∀𝑥𝑥 = 𝑦 → ∀𝑥∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑢))
15:1,141:	⊢ ( ∀𝑥𝑥 = 𝑦 ▶ ∀𝑥∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑢) )
16:1,15:	⊢ ( ∀𝑥𝑥 = 𝑦 ▶ ∀𝑦∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑢) )
17:16:	⊢ ( ∀𝑥𝑥 = 𝑦 ▶ ∃𝑦∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑢) )
18:17:	⊢ ( ∀𝑥𝑥 = 𝑦 ▶ ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑢) )
19::	⊢ ( 𝑢 = 𝑣 ▶ 𝑢 = 𝑣 )
20::	⊢ ( 𝑢 = 𝑣 , (𝑥 = 𝑢 ∧ 𝑦 = 𝑢) ▶ (𝑥 = 𝑢 ∧ 𝑦 = 𝑢) )
21:20:	⊢ ( 𝑢 = 𝑣 , (𝑥 = 𝑢 ∧ 𝑦 = 𝑢) ▶ 𝑦 = 𝑢 )
22:19,21:	⊢ ( 𝑢 = 𝑣 , (𝑥 = 𝑢 ∧ 𝑦 = 𝑢) ▶ 𝑦 = 𝑣 )
23:20:	⊢ ( 𝑢 = 𝑣 , (𝑥 = 𝑢 ∧ 𝑦 = 𝑢) ▶ 𝑥 = 𝑢 )
24:22,23:	⊢ ( 𝑢 = 𝑣 , (𝑥 = 𝑢 ∧ 𝑦 = 𝑢) ▶ (𝑥 = 𝑢 ∧ 𝑦 = 𝑣) )
25:24:	⊢ ( 𝑢 = 𝑣 ▶ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣)) )
26:25:	⊢ ( 𝑢 = 𝑣 ▶ ∀𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → (𝑥 = 𝑢 ∧ 𝑦 = 𝑣)) )
27:26:	⊢ ( 𝑢 = 𝑣 ▶ (∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → ∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣)) )
28:27:	⊢ ( 𝑢 = 𝑣 ▶ ∀𝑥(∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → ∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣)) )
29:28:	⊢ ( 𝑢 = 𝑣 ▶ (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣)) )
30:29:	⊢ (𝑢 = 𝑣 → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑢 ) → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣)))
31:18,30:	⊢ ( ∀𝑥𝑥 = 𝑦 ▶ (𝑢 = 𝑣 → ∃𝑥∃𝑦 (𝑥 = 𝑢 ∧ 𝑦 = 𝑣)) )
qed:31:	⊢ (∀𝑥𝑥 = 𝑦 → (𝑢 = 𝑣 → ∃𝑥∃𝑦( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣)))

(∀𝑥 𝑥 = 𝑦 → (𝑢 = 𝑣 → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣)))

Theorem

ax6e2ndVD 44904*

The following User's Proof is a Virtual Deduction proof (see wvd1 44566) completed automatically by a Metamath tools program invoking mmj2 and the Metamath Proof Assistant. ax6e2nd 44555 is ax6e2ndVD 44904 without virtual deductions and was automatically derived from ax6e2ndVD 44904. (Contributed by Alan Sare, 25-Mar-2014.) (Proof modification is discouraged.) (New usage is discouraged.)

1::	⊢ ∃𝑦𝑦 = 𝑣
2::	⊢ 𝑢 ∈ V
3:1,2:	⊢ (𝑢 ∈ V ∧ ∃𝑦𝑦 = 𝑣)
4:3:	⊢ ∃𝑦(𝑢 ∈ V ∧ 𝑦 = 𝑣)
5::	⊢ (𝑢 ∈ V ↔ ∃𝑥𝑥 = 𝑢)
6:5:	⊢ ((𝑢 ∈ V ∧ 𝑦 = 𝑣) ↔ (∃𝑥𝑥 = 𝑢 ∧ 𝑦 = 𝑣))
7:6:	⊢ (∃𝑦(𝑢 ∈ V ∧ 𝑦 = 𝑣) ↔ ∃𝑦 (∃𝑥𝑥 = 𝑢 ∧ 𝑦 = 𝑣))
8:4,7:	⊢ ∃𝑦(∃𝑥𝑥 = 𝑢 ∧ 𝑦 = 𝑣)
9::	⊢ (𝑧 = 𝑣 → ∀𝑥𝑧 = 𝑣)
10::	⊢ (𝑦 = 𝑣 → ∀𝑧𝑦 = 𝑣)
11::	⊢ ( 𝑧 = 𝑦 ▶ 𝑧 = 𝑦 )
12:11:	⊢ ( 𝑧 = 𝑦 ▶ (𝑧 = 𝑣 ↔ 𝑦 = 𝑣) )
120:11:	⊢ (𝑧 = 𝑦 → (𝑧 = 𝑣 ↔ 𝑦 = 𝑣))
13:9,10,120:	⊢ (¬ ∀𝑥𝑥 = 𝑦 → (𝑦 = 𝑣 → ∀𝑥𝑦 = 𝑣))
14::	⊢ ( ¬ ∀𝑥𝑥 = 𝑦 ▶ ¬ ∀𝑥𝑥 = 𝑦 )
15:14,13:	⊢ ( ¬ ∀𝑥𝑥 = 𝑦 ▶ (𝑦 = 𝑣 → ∀𝑥 𝑦 = 𝑣) )
16:15:	⊢ (¬ ∀𝑥𝑥 = 𝑦 → (𝑦 = 𝑣 → ∀𝑥𝑦 = 𝑣))
17:16:	⊢ (∀𝑥¬ ∀𝑥𝑥 = 𝑦 → ∀𝑥(𝑦 = 𝑣 → ∀𝑥𝑦 = 𝑣))
18::	⊢ (¬ ∀𝑥𝑥 = 𝑦 → ∀𝑥¬ ∀𝑥𝑥 = 𝑦 )
19:17,18:	⊢ (¬ ∀𝑥𝑥 = 𝑦 → ∀𝑥(𝑦 = 𝑣 → ∀ 𝑥𝑦 = 𝑣))
20:14,19:	⊢ ( ¬ ∀𝑥𝑥 = 𝑦 ▶ ∀𝑥(𝑦 = 𝑣 → ∀𝑥𝑦 = 𝑣) )
21:20:	⊢ ( ¬ ∀𝑥𝑥 = 𝑦 ▶ ((∃𝑥𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣)) )
22:21:	⊢ (¬ ∀𝑥𝑥 = 𝑦 → ((∃𝑥𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣)))
23:22:	⊢ (∀𝑦¬ ∀𝑥𝑥 = 𝑦 → ∀𝑦((∃𝑥 𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣)))
24::	⊢ (¬ ∀𝑥𝑥 = 𝑦 → ∀𝑦¬ ∀𝑥𝑥 = 𝑦 )
25:23,24:	⊢ (¬ ∀𝑥𝑥 = 𝑦 → ∀𝑦((∃𝑥𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣)))
26:14,25:	⊢ ( ¬ ∀𝑥𝑥 = 𝑦 ▶ ∀𝑦((∃𝑥𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣)) )
27:26:	⊢ ( ¬ ∀𝑥𝑥 = 𝑦 ▶ (∃𝑦(∃𝑥𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑦∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣)) )
28:8,27:	⊢ ( ¬ ∀𝑥𝑥 = 𝑦 ▶ ∃𝑦∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) )
29:28:	⊢ ( ¬ ∀𝑥𝑥 = 𝑦 ▶ ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) )
qed:29:	⊢ (¬ ∀𝑥𝑥 = 𝑦 → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))

(¬ ∀𝑥 𝑥 = 𝑦 → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))

Theorem

ax6e2ndeqVD 44905*

The following User's Proof is a Virtual Deduction proof (see wvd1 44566) completed automatically by a Metamath tools program invoking mmj2 and the Metamath Proof Assistant. ax6e2eq 44554 is ax6e2ndeqVD 44905 without virtual deductions and was automatically derived from ax6e2ndeqVD 44905. (Contributed by Alan Sare, 25-Mar-2014.) (Proof modification is discouraged.) (New usage is discouraged.)

1::	⊢ ( 𝑢 ≠ 𝑣 ▶ 𝑢 ≠ 𝑣 )
2::	⊢ ( 𝑢 ≠ 𝑣 , (𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ▶ ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣) )
3:2:	⊢ ( 𝑢 ≠ 𝑣 , (𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ▶ 𝑥 = 𝑢 )
4:1,3:	⊢ ( 𝑢 ≠ 𝑣 , (𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ▶ 𝑥 ≠ 𝑣 )
5:2:	⊢ ( 𝑢 ≠ 𝑣 , (𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ▶ 𝑦 = 𝑣 )
6:4,5:	⊢ ( 𝑢 ≠ 𝑣 , (𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ▶ 𝑥 ≠ 𝑦 )
7::	⊢ (∀𝑥𝑥 = 𝑦 → 𝑥 = 𝑦)
8:7:	⊢ (¬ 𝑥 = 𝑦 → ¬ ∀𝑥𝑥 = 𝑦)
9::	⊢ (¬ 𝑥 = 𝑦 ↔ 𝑥 ≠ 𝑦)
10:8,9:	⊢ (𝑥 ≠ 𝑦 → ¬ ∀𝑥𝑥 = 𝑦)
11:6,10:	⊢ ( 𝑢 ≠ 𝑣 , (𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ▶ ¬ ∀𝑥𝑥 = 𝑦 )
12:11:	⊢ ( 𝑢 ≠ 𝑣 ▶ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ¬ ∀𝑥𝑥 = 𝑦) )
13:12:	⊢ ( 𝑢 ≠ 𝑣 ▶ ∀𝑥((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ¬ ∀𝑥𝑥 = 𝑦) )
14:13:	⊢ ( 𝑢 ≠ 𝑣 ▶ (∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑥¬ ∀𝑥𝑥 = 𝑦) )
15::	⊢ (¬ ∀𝑥𝑥 = 𝑦 → ∀𝑥¬ ∀𝑥𝑥 = 𝑦 )
19:15:	⊢ (∃𝑥¬ ∀𝑥𝑥 = 𝑦 ↔ ¬ ∀𝑥𝑥 = 𝑦)
20:14,19:	⊢ ( 𝑢 ≠ 𝑣 ▶ (∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ¬ ∀𝑥𝑥 = 𝑦) )
21:20:	⊢ ( 𝑢 ≠ 𝑣 ▶ ∀𝑦(∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ¬ ∀𝑥𝑥 = 𝑦) )
22:21:	⊢ ( 𝑢 ≠ 𝑣 ▶ (∃𝑦∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑦¬ ∀𝑥𝑥 = 𝑦) )
23::	⊢ (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ↔ ∃ 𝑦∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))
24:22,23:	⊢ ( 𝑢 ≠ 𝑣 ▶ (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑦¬ ∀𝑥𝑥 = 𝑦) )
25::	⊢ (¬ ∀𝑥𝑥 = 𝑦 → ∀𝑦¬ ∀𝑥𝑥 = 𝑦 )
26:25:	⊢ (∃𝑦¬ ∀𝑥𝑥 = 𝑦 → ∃𝑦∀𝑦¬ ∀𝑥𝑥 = 𝑦)
260::	⊢ (∀𝑦¬ ∀𝑥𝑥 = 𝑦 → ∀𝑦∀𝑦¬ ∀𝑥𝑥 = 𝑦)
27:260:	⊢ (∃𝑦∀𝑦¬ ∀𝑥𝑥 = 𝑦 ↔ ∀𝑦¬ ∀𝑥𝑥 = 𝑦)
270:26,27:	⊢ (∃𝑦¬ ∀𝑥𝑥 = 𝑦 → ∀𝑦¬ ∀𝑥 𝑥 = 𝑦)
28::	⊢ (∀𝑦¬ ∀𝑥𝑥 = 𝑦 → ¬ ∀𝑥𝑥 = 𝑦 )
29:270,28:	⊢ (∃𝑦¬ ∀𝑥𝑥 = 𝑦 → ¬ ∀𝑥𝑥 = 𝑦 )
30:24,29:	⊢ ( 𝑢 ≠ 𝑣 ▶ (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ¬ ∀𝑥𝑥 = 𝑦) )
31:30:	⊢ ( 𝑢 ≠ 𝑣 ▶ (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (¬ ∀𝑥𝑥 = 𝑦 ∨ 𝑢 = 𝑣)) )
32:31:	⊢ (𝑢 ≠ 𝑣 → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (¬ ∀𝑥𝑥 = 𝑦 ∨ 𝑢 = 𝑣)))
33::	⊢ ( 𝑢 = 𝑣 ▶ 𝑢 = 𝑣 )
34:33:	⊢ ( 𝑢 = 𝑣 ▶ (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → 𝑢 = 𝑣) )
35:34:	⊢ ( 𝑢 = 𝑣 ▶ (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (¬ ∀𝑥𝑥 = 𝑦 ∨ 𝑢 = 𝑣)) )
36:35:	⊢ (𝑢 = 𝑣 → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (¬ ∀𝑥𝑥 = 𝑦 ∨ 𝑢 = 𝑣)))
37::	⊢ (𝑢 = 𝑣 ∨ 𝑢 ≠ 𝑣)
38:32,36,37:	⊢ (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ( ¬ ∀𝑥𝑥 = 𝑦 ∨ 𝑢 = 𝑣))
39::	⊢ (∀𝑥𝑥 = 𝑦 → (𝑢 = 𝑣 → ∃𝑥∃𝑦 (𝑥 = 𝑢 ∧ 𝑦 = 𝑣)))
40::	⊢ (¬ ∀𝑥𝑥 = 𝑦 → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))
41:40:	⊢ (¬ ∀𝑥𝑥 = 𝑦 → (𝑢 = 𝑣 → ∃𝑥∃ 𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣)))
42::	⊢ (∀𝑥𝑥 = 𝑦 ∨ ¬ ∀𝑥𝑥 = 𝑦)
43:39,41,42:	⊢ (𝑢 = 𝑣 → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ))
44:40,43:	⊢ ((¬ ∀𝑥𝑥 = 𝑦 ∨ 𝑢 = 𝑣) → ∃𝑥 ∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))
qed:38,44:	⊢ ((¬ ∀𝑥𝑥 = 𝑦 ∨ 𝑢 = 𝑣) ↔ ∃𝑥 ∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))

((¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣) ↔ ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))

Theorem

2sb5ndVD 44906*

The following User's Proof is a Virtual Deduction proof (see wvd1 44566) completed automatically by a Metamath tools program invoking mmj2 and the Metamath Proof Assistant. 2sb5nd 44557 is 2sb5ndVD 44906 without virtual deductions and was automatically derived from 2sb5ndVD 44906. (Contributed by Alan Sare, 30-Apr-2014.) (Proof modification is discouraged.) (New usage is discouraged.)

1::	⊢ (((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][ 𝑣 / 𝑦]𝜑) ↔ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑))
2:1:	⊢ (∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑) ↔ ∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑))
3::	⊢ ([𝑣 / 𝑦]𝜑 → ∀𝑦[𝑣 / 𝑦]𝜑)
4:3:	⊢ [𝑢 / 𝑥]([𝑣 / 𝑦]𝜑 → ∀𝑦[𝑣 / 𝑦]𝜑)
5:4:	⊢ ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → [𝑢 / 𝑥] ∀𝑦[𝑣 / 𝑦]𝜑)
6::	⊢ ( ¬ ∀𝑥𝑥 = 𝑦 ▶ ¬ ∀𝑥𝑥 = 𝑦 )
7::	⊢ (∀𝑦𝑦 = 𝑥 → ∀𝑥𝑥 = 𝑦)
8:7:	⊢ (¬ ∀𝑥𝑥 = 𝑦 → ¬ ∀𝑦𝑦 = 𝑥)
9:6,8:	⊢ ( ¬ ∀𝑥𝑥 = 𝑦 ▶ ¬ ∀𝑦𝑦 = 𝑥 )
10:9:	⊢ ([𝑢 / 𝑥]∀𝑦[𝑣 / 𝑦]𝜑 ↔ ∀ 𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑)
11:5,10:	⊢ ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑)
12:11:	⊢ (¬ ∀𝑥𝑥 = 𝑦 → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
13::	⊢ ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ∀𝑥[𝑢 / 𝑥][𝑣 / 𝑦]𝜑)
14::	⊢ ( ∀𝑥𝑥 = 𝑦 ▶ ∀𝑥𝑥 = 𝑦 )
15:14:	⊢ ( ∀𝑥𝑥 = 𝑦 ▶ (∀𝑥[𝑢 / 𝑥][ 𝑣 / 𝑦]𝜑 → ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑) )
16:13,15:	⊢ ( ∀𝑥𝑥 = 𝑦 ▶ ([𝑢 / 𝑥][𝑣 / 𝑦 ]𝜑 → ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑) )
17:16:	⊢ (∀𝑥𝑥 = 𝑦 → ([𝑢 / 𝑥][𝑣 / 𝑦] 𝜑 → ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
19:12,17:	⊢ ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑)
20:19:	⊢ (∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑) ↔ (∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
21:2,20:	⊢ (∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑) ↔ (∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
22:21:	⊢ (∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑) ↔ ∃𝑥(∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
23:13:	⊢ (∃𝑥(∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [ 𝑢 / 𝑥][𝑣 / 𝑦]𝜑) ↔ (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
24:22,23:	⊢ ((∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [ 𝑢 / 𝑥][𝑣 / 𝑦]𝜑) ↔ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑))
240:24:	⊢ ((∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ ( ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑)) ↔ (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑)))
241::	⊢ ((∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ ( ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑)) ↔ (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
242:241,240:	⊢ ((∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [ 𝑢 / 𝑥][𝑣 / 𝑦]𝜑) ↔ (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑)))
243::	⊢ ((∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ( [𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ↔ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑))) ↔ ((∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑) ↔ (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑))))
25:242,243:	⊢ (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ([ 𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ↔ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑)))
26::	⊢ ((¬ ∀𝑥𝑥 = 𝑦 ∨ 𝑢 = 𝑣) ↔ ∃𝑥 ∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))
qed:25,26:	⊢ ((¬ ∀𝑥𝑥 = 𝑦 ∨ 𝑢 = 𝑣) → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ↔ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑)))

((¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣) → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ↔ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑)))

Theorem

2uasbanhVD 44907*

The following User's Proof is a Virtual Deduction proof (see wvd1 44566) completed automatically by a Metamath tools program invoking mmj2 and the Metamath Proof Assistant. 2uasbanh 44558 is 2uasbanhVD 44907 without virtual deductions and was automatically derived from 2uasbanhVD 44907. (Contributed by Alan Sare, 31-May-2014.) (Proof modification is discouraged.) (New usage is discouraged.)

h1::	⊢ (𝜒 ↔ (∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑) ∧ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜓)))
100:1:	⊢ (𝜒 → (∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑) ∧ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜓)))
2:100:	⊢ ( 𝜒 ▶ (∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑) ∧ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜓)) )
3:2:	⊢ ( 𝜒 ▶ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑) )
4:3:	⊢ ( 𝜒 ▶ ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) )
5:4:	⊢ ( 𝜒 ▶ (¬ ∀𝑥𝑥 = 𝑦 ∨ 𝑢 = 𝑣) )
6:5:	⊢ ( 𝜒 ▶ ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ↔ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑)) )
7:3,6:	⊢ ( 𝜒 ▶ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑 )
8:2:	⊢ ( 𝜒 ▶ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜓) )
9:5:	⊢ ( 𝜒 ▶ ([𝑢 / 𝑥][𝑣 / 𝑦]𝜓 ↔ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜓)) )
10:8,9:	⊢ ( 𝜒 ▶ [𝑢 / 𝑥][𝑣 / 𝑦]𝜓 )
101::	⊢ ([𝑣 / 𝑦](𝜑 ∧ 𝜓) ↔ ([𝑣 / 𝑦]𝜑 ∧ [𝑣 / 𝑦]𝜓))
102:101:	⊢ ([𝑢 / 𝑥][𝑣 / 𝑦](𝜑 ∧ 𝜓) ↔ [𝑢 / 𝑥]([𝑣 / 𝑦]𝜑 ∧ [𝑣 / 𝑦]𝜓))
103::	⊢ ([𝑢 / 𝑥]([𝑣 / 𝑦]𝜑 ∧ [𝑣 / 𝑦 ]𝜓) ↔ ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜓))
104:102,103:	⊢ ([𝑢 / 𝑥][𝑣 / 𝑦](𝜑 ∧ 𝜓) ↔ ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜓))
11:7,10,104:	⊢ ( 𝜒 ▶ [𝑢 / 𝑥][𝑣 / 𝑦](𝜑 ∧ 𝜓) )
110:5:	⊢ ( 𝜒 ▶ ([𝑢 / 𝑥][𝑣 / 𝑦](𝜑 ∧ 𝜓) ↔ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ (𝜑 ∧ 𝜓))) )
12:11,110:	⊢ ( 𝜒 ▶ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ (𝜑 ∧ 𝜓)) )
120:12:	⊢ (𝜒 → ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ (𝜑 ∧ 𝜓)))
13:1,120:	⊢ ((∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑) ∧ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜓)) → ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ (𝜑 ∧ 𝜓)))
14::	⊢ ( ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ (𝜑 ∧ 𝜓 )) ▶ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ (𝜑 ∧ 𝜓)) )
15:14:	⊢ ( ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ (𝜑 ∧ 𝜓 )) ▶ (𝑥 = 𝑢 ∧ 𝑦 = 𝑣) )
16:14:	⊢ ( ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ (𝜑 ∧ 𝜓 )) ▶ (𝜑 ∧ 𝜓) )
17:16:	⊢ ( ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ (𝜑 ∧ 𝜓 )) ▶ 𝜑 )
18:15,17:	⊢ ( ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ (𝜑 ∧ 𝜓 )) ▶ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑) )
19:18:	⊢ (((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ (𝜑 ∧ 𝜓 )) → ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑))
20:19:	⊢ (∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ (𝜑 ∧ 𝜓)) → ∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑))
21:20:	⊢ (∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ ( 𝜑 ∧ 𝜓)) → ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑))
22:16:	⊢ ( ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ (𝜑 ∧ 𝜓 )) ▶ 𝜓 )
23:15,22:	⊢ ( ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ (𝜑 ∧ 𝜓 )) ▶ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜓) )
24:23:	⊢ (((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ (𝜑 ∧ 𝜓 )) → ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜓))
25:24:	⊢ (∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ (𝜑 ∧ 𝜓)) → ∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜓))
26:25:	⊢ (∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ ( 𝜑 ∧ 𝜓)) → ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜓))
27:21,26:	⊢ (∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ ( 𝜑 ∧ 𝜓)) → (∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑) ∧ ∃𝑥∃𝑦( (𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜓)))
qed:13,27:	⊢ (∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ ( 𝜑 ∧ 𝜓)) ↔ (∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑) ∧ ∃𝑥∃𝑦( (𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜓)))

(𝜒 ↔ (∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑) ∧ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜓))) ⇒ (∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ (𝜑 ∧ 𝜓)) ↔ (∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑) ∧ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜓)))

Theorem

e2ebindVD 44908

The following User's Proof is a Virtual Deduction proof (see wvd1 44566) completed automatically by a Metamath tools program invoking mmj2 and the Metamath Proof Assistant. e2ebind 44560 is e2ebindVD 44908 without virtual deductions and was automatically derived from e2ebindVD 44908.

1::	⊢ (𝜑 ↔ 𝜑)
2:1:	⊢ (∀𝑦𝑦 = 𝑥 → (𝜑 ↔ 𝜑))
3:2:	⊢ (∀𝑦𝑦 = 𝑥 → (∃𝑦𝜑 ↔ ∃𝑥𝜑 ))
4::	⊢ ( ∀𝑦𝑦 = 𝑥 ▶ ∀𝑦𝑦 = 𝑥 )
5:3,4:	⊢ ( ∀𝑦𝑦 = 𝑥 ▶ (∃𝑦𝜑 ↔ ∃𝑥 𝜑) )
6::	⊢ (∀𝑦𝑦 = 𝑥 → ∀𝑦∀𝑦𝑦 = 𝑥)
7:5,6:	⊢ ( ∀𝑦𝑦 = 𝑥 ▶ ∀𝑦(∃𝑦𝜑 ↔ ∃𝑥𝜑) )
8:7:	⊢ ( ∀𝑦𝑦 = 𝑥 ▶ (∃𝑦∃𝑦𝜑 ↔ ∃𝑦∃𝑥𝜑) )
9::	⊢ (∃𝑦∃𝑥𝜑 ↔ ∃𝑥∃𝑦𝜑)
10:8,9:	⊢ ( ∀𝑦𝑦 = 𝑥 ▶ (∃𝑦∃𝑦𝜑 ↔ ∃𝑥∃𝑦𝜑) )
11::	⊢ (∃𝑦𝜑 → ∀𝑦∃𝑦𝜑)
12:11:	⊢ (∃𝑦∃𝑦𝜑 ↔ ∃𝑦𝜑)
13:10,12:	⊢ ( ∀𝑦𝑦 = 𝑥 ▶ (∃𝑥∃𝑦𝜑 ↔ ∃𝑦𝜑) )
14:13:	⊢ (∀𝑦𝑦 = 𝑥 → (∃𝑥∃𝑦𝜑 ↔ ∃ 𝑦𝜑))
15::	⊢ (∀𝑦𝑦 = 𝑥 ↔ ∀𝑥𝑥 = 𝑦)
qed:14,15:	⊢ (∀𝑥𝑥 = 𝑦 → (∃𝑥∃𝑦𝜑 ↔ ∃ 𝑦𝜑))

(Contributed by Alan Sare, 27-Nov-2014.) (Proof modification is discouraged.) (New usage is discouraged.)

(∀𝑥 𝑥 = 𝑦 → (∃𝑥∃𝑦𝜑 ↔ ∃𝑦𝜑))

21.41.8 Virtual Deduction transcriptions of textbook proofs

Theorem

sb5ALTVD 44909*

The following User's Proof is a Natural Deduction Sequent Calculus transcription of the Fitch-style Natural Deduction proof of Unit 20 Excercise 3.a., which is sb5 2276, found in the "Answers to Starred Exercises" on page 457 of "Understanding Symbolic Logic", Fifth Edition (2008), by Virginia Klenk. The same proof may also be interpreted as a Virtual Deduction Hilbert-style axiomatic proof. It was completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. sb5ALT 44522 is sb5ALTVD 44909 without virtual deductions and was automatically derived from sb5ALTVD 44909.

1::	⊢ ( [𝑦 / 𝑥]𝜑 ▶ [𝑦 / 𝑥]𝜑 )
2::	⊢ [𝑦 / 𝑥]𝑥 = 𝑦
3:1,2:	⊢ ( [𝑦 / 𝑥]𝜑 ▶ [𝑦 / 𝑥](𝑥 = 𝑦 ∧ 𝜑) )
4:3:	⊢ ( [𝑦 / 𝑥]𝜑 ▶ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑 ) )
5:4:	⊢ ([𝑦 / 𝑥]𝜑 → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑) )
6::	⊢ ( ∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ▶ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑) )
7::	⊢ ( ∃𝑥(𝑥 = 𝑦 ∧ 𝜑) , (𝑥 = 𝑦 ∧ 𝜑 ) ▶ (𝑥 = 𝑦 ∧ 𝜑) )
8:7:	⊢ ( ∃𝑥(𝑥 = 𝑦 ∧ 𝜑) , (𝑥 = 𝑦 ∧ 𝜑 ) ▶ 𝜑 )
9:7:	⊢ ( ∃𝑥(𝑥 = 𝑦 ∧ 𝜑) , (𝑥 = 𝑦 ∧ 𝜑 ) ▶ 𝑥 = 𝑦 )
10:8,9:	⊢ ( ∃𝑥(𝑥 = 𝑦 ∧ 𝜑) , (𝑥 = 𝑦 ∧ 𝜑 ) ▶ [𝑦 / 𝑥]𝜑 )
101::	⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑)
11:101,10:	⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → [𝑦 / 𝑥]𝜑 )
12:5,11:	⊢ (([𝑦 / 𝑥]𝜑 → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑 )) ∧ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → [𝑦 / 𝑥]𝜑))
qed:12:	⊢ ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑) )

(Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.)

([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))

Theorem

vk15.4jVD 44910

The following User's Proof is a Natural Deduction Sequent Calculus transcription of the Fitch-style Natural Deduction proof of Unit 15 Excercise 4.f. found in the "Answers to Starred Exercises" on page 442 of "Understanding Symbolic Logic", Fifth Edition (2008), by Virginia Klenk. The same proof may also be interpreted to be a Virtual Deduction Hilbert-style axiomatic proof. It was completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. vk15.4j 44525 is vk15.4jVD 44910 without virtual deductions and was automatically derived from vk15.4jVD 44910. Step numbers greater than 25 are additional steps necessary for the sequent calculus proof not contained in the Fitch-style proof. Otherwise, step i of the User's Proof corresponds to step i of the Fitch-style proof.

h1::	⊢ ¬ (∃𝑥¬ 𝜑 ∧ ∃𝑥(𝜓 ∧ ¬ 𝜒))
h2::	⊢ (∀𝑥𝜒 → ¬ ∃𝑥(𝜃 ∧ 𝜏 ))
h3::	⊢ ¬ ∀𝑥(𝜏 → 𝜑)
4::	⊢ ( ¬ ∃𝑥¬ 𝜃 ▶ ¬ ∃𝑥¬ 𝜃 )
5:4:	⊢ ( ¬ ∃𝑥¬ 𝜃 ▶ ∀𝑥𝜃 )
6:3:	⊢ ∃𝑥(𝜏 ∧ ¬ 𝜑)
7::	⊢ ( ¬ ∃𝑥¬ 𝜃 , (𝜏 ∧ ¬ 𝜑) ▶ (𝜏 ∧ ¬ 𝜑) )
8:7:	⊢ ( ¬ ∃𝑥¬ 𝜃 , (𝜏 ∧ ¬ 𝜑) ▶ 𝜏 )
9:7:	⊢ ( ¬ ∃𝑥¬ 𝜃 , (𝜏 ∧ ¬ 𝜑) ▶ ¬ 𝜑 )
10:5:	⊢ ( ¬ ∃𝑥¬ 𝜃 ▶ 𝜃 )
11:10,8:	⊢ ( ¬ ∃𝑥¬ 𝜃 , (𝜏 ∧ ¬ 𝜑) ▶ (𝜃 ∧ 𝜏) )
12:11:	⊢ ( ¬ ∃𝑥¬ 𝜃 , (𝜏 ∧ ¬ 𝜑) ▶ ∃𝑥(𝜃 ∧ 𝜏) )
13:12:	⊢ ( ¬ ∃𝑥¬ 𝜃 , (𝜏 ∧ ¬ 𝜑) ▶ ¬ ¬ ∃𝑥(𝜃 ∧ 𝜏) )
14:2,13:	⊢ ( ¬ ∃𝑥¬ 𝜃 , (𝜏 ∧ ¬ 𝜑) ▶ ¬ ∀𝑥𝜒 )
140::	⊢ (∃𝑥¬ 𝜃 → ∀𝑥∃𝑥¬ 𝜃 )
141:140:	⊢ (¬ ∃𝑥¬ 𝜃 → ∀𝑥¬ ∃𝑥 ¬ 𝜃)
142::	⊢ (∀𝑥𝜒 → ∀𝑥∀𝑥𝜒)
143:142:	⊢ (¬ ∀𝑥𝜒 → ∀𝑥¬ ∀𝑥𝜒 )
144:6,14,141,143:	⊢ ( ¬ ∃𝑥¬ 𝜃 ▶ ¬ ∀𝑥𝜒 )
15:1:	⊢ (¬ ∃𝑥¬ 𝜑 ∨ ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒))
16:9:	⊢ ( ¬ ∃𝑥¬ 𝜃 , (𝜏 ∧ ¬ 𝜑) ▶ ∃𝑥¬ 𝜑 )
161::	⊢ (∃𝑥¬ 𝜑 → ∀𝑥∃𝑥¬ 𝜑 )
162:6,16,141,161:	⊢ ( ¬ ∃𝑥¬ 𝜃 ▶ ∃𝑥¬ 𝜑 )
17:162:	⊢ ( ¬ ∃𝑥¬ 𝜃 ▶ ¬ ¬ ∃𝑥 ¬ 𝜑 )
18:15,17:	⊢ ( ¬ ∃𝑥¬ 𝜃 ▶ ¬ ∃𝑥( 𝜓 ∧ ¬ 𝜒) )
19:18:	⊢ ( ¬ ∃𝑥¬ 𝜃 ▶ ∀𝑥(𝜓 → 𝜒) )
20:144:	⊢ ( ¬ ∃𝑥¬ 𝜃 ▶ ∃𝑥¬ 𝜒 )
21::	⊢ ( ¬ ∃𝑥¬ 𝜃 , ¬ 𝜒 ▶ ¬ 𝜒 )
22:19:	⊢ ( ¬ ∃𝑥¬ 𝜃 ▶ (𝜓 → 𝜒 ) )
23:21,22:	⊢ ( ¬ ∃𝑥¬ 𝜃 , ¬ 𝜒 ▶ ¬ 𝜓 )
24:23:	⊢ ( ¬ ∃𝑥¬ 𝜃 , ¬ 𝜒 ▶ ∃ 𝑥¬ 𝜓 )
240::	⊢ (∃𝑥¬ 𝜓 → ∀𝑥∃𝑥¬ 𝜓 )
241:20,24,141,240:	⊢ ( ¬ ∃𝑥¬ 𝜃 ▶ ∃𝑥¬ 𝜓 )
25:241:	⊢ ( ¬ ∃𝑥¬ 𝜃 ▶ ¬ ∀𝑥𝜓 )
qed:25:	⊢ (¬ ∃𝑥¬ 𝜃 → ¬ ∀𝑥𝜓)

(Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.)

¬ (∃𝑥 ¬ 𝜑 ∧ ∃𝑥(𝜓 ∧ ¬ 𝜒)) & (∀𝑥𝜒 → ¬ ∃𝑥(𝜃 ∧ 𝜏)) & ¬ ∀𝑥(𝜏 → 𝜑) ⇒ (¬ ∃𝑥 ¬ 𝜃 → ¬ ∀𝑥𝜓)

Theorem

notnotrALTVD 44911

The following User's Proof is a Natural Deduction Sequent Calculus transcription of the Fitch-style Natural Deduction proof of Theorem 5 of Section 14 of [Margaris] p. 59 (which is notnotr 130). The same proof may also be interpreted as a Virtual Deduction Hilbert-style axiomatic proof. It was completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. notnotrALT 44526 is notnotrALTVD 44911 without virtual deductions and was automatically derived from notnotrALTVD 44911. Step i of the User's Proof corresponds to step i of the Fitch-style proof.

1::	⊢ ( ¬ ¬ 𝜑 ▶ ¬ ¬ 𝜑 )
2::	⊢ (¬ ¬ 𝜑 → (¬ 𝜑 → ¬ ¬ ¬ 𝜑))
3:1:	⊢ ( ¬ ¬ 𝜑 ▶ (¬ 𝜑 → ¬ ¬ ¬ 𝜑) )
4::	⊢ ((¬ 𝜑 → ¬ ¬ ¬ 𝜑) → (¬ ¬ 𝜑 → 𝜑))
5:3:	⊢ ( ¬ ¬ 𝜑 ▶ (¬ ¬ 𝜑 → 𝜑) )
6:5,1:	⊢ ( ¬ ¬ 𝜑 ▶ 𝜑 )
qed:6:	⊢ (¬ ¬ 𝜑 → 𝜑)

(Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.)

(¬ ¬ 𝜑 → 𝜑)

Theorem

con3ALTVD 44912

The following User's Proof is a Natural Deduction Sequent Calculus transcription of the Fitch-style Natural Deduction proof of Theorem 7 of Section 14 of [Margaris] p. 60 (which is con3 153). The same proof may also be interpreted to be a Virtual Deduction Hilbert-style axiomatic proof. It was completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. con3ALT2 44527 is con3ALTVD 44912 without virtual deductions and was automatically derived from con3ALTVD 44912. Step i of the User's Proof corresponds to step i of the Fitch-style proof.

1::	⊢ ( (𝜑 → 𝜓) ▶ (𝜑 → 𝜓) )
2::	⊢ ( (𝜑 → 𝜓) , ¬ ¬ 𝜑 ▶ ¬ ¬ 𝜑 )
3::	⊢ (¬ ¬ 𝜑 → 𝜑)
4:2:	⊢ ( (𝜑 → 𝜓) , ¬ ¬ 𝜑 ▶ 𝜑 )
5:1,4:	⊢ ( (𝜑 → 𝜓) , ¬ ¬ 𝜑 ▶ 𝜓 )
6::	⊢ (𝜓 → ¬ ¬ 𝜓)
7:6,5:	⊢ ( (𝜑 → 𝜓) , ¬ ¬ 𝜑 ▶ ¬ ¬ 𝜓 )
8:7:	⊢ ( (𝜑 → 𝜓) ▶ (¬ ¬ 𝜑 → ¬ ¬ 𝜓 ) )
9::	⊢ ((¬ ¬ 𝜑 → ¬ ¬ 𝜓) → (¬ 𝜓 → ¬ 𝜑))
10:8:	⊢ ( (𝜑 → 𝜓) ▶ (¬ 𝜓 → ¬ 𝜑) )
qed:10:	⊢ ((𝜑 → 𝜓) → (¬ 𝜓 → ¬ 𝜑))

(Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.)

((𝜑 → 𝜓) → (¬ 𝜓 → ¬ 𝜑))

21.41.9 Theorems proved using conjunction-form Virtual Deduction

Theorem

elpwgdedVD 44913

Membership in a power class. Theorem 86 of [Suppes] p. 47. Derived from elpwg 4569. In form of VD deduction with 𝜑 and 𝜓 as variable virtual hypothesis collections based on Mario Carneiro's metavariable concept. elpwgded 44561 is elpwgdedVD 44913 using conventional notation. (Contributed by Alan Sare, 23-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.)

( 𝜑 ▶ 𝐴 ∈ V ) & ( 𝜓 ▶ 𝐴 ⊆ 𝐵 ) ⇒ ( ( 𝜑 , 𝜓 ) ▶ 𝐴 ∈ 𝒫 𝐵 )

Theorem

sspwimp 44914

If a class is a subclass of another class, then its power class is a subclass of that other class's power class. Left-to-right implication of Exercise 18 of [TakeutiZaring] p. 18. For the biconditional, see sspwb 5412. The proof sspwimp 44914, using conventional notation, was translated from virtual deduction form, sspwimpVD 44915, using a translation program. (Contributed by Alan Sare, 23-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.)

(𝐴 ⊆ 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵)

Theorem

sspwimpVD 44915

The following User's Proof is a Virtual Deduction proof (see wvd1 44566) using conjunction-form virtual hypothesis collections. It was completed manually, but has the potential to be completed automatically by a tools program which would invoke Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. sspwimp 44914 is sspwimpVD 44915 without virtual deductions and was derived from sspwimpVD 44915. (Contributed by Alan Sare, 23-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.)

1::	⊢ ( 𝐴 ⊆ 𝐵 ▶ 𝐴 ⊆ 𝐵 )
2::	⊢ ( .............. 𝑥 ∈ 𝒫 𝐴 ▶ 𝑥 ∈ 𝒫 𝐴 )
3:2:	⊢ ( .............. 𝑥 ∈ 𝒫 𝐴 ▶ 𝑥 ⊆ 𝐴 )
4:3,1:	⊢ ( ( 𝐴 ⊆ 𝐵 , 𝑥 ∈ 𝒫 𝐴 ) ▶ 𝑥 ⊆ 𝐵 )
5::	⊢ 𝑥 ∈ V
6:4,5:	⊢ ( ( 𝐴 ⊆ 𝐵 , 𝑥 ∈ 𝒫 𝐴 ) ▶ 𝑥 ∈ 𝒫 𝐵 )
7:6:	⊢ ( 𝐴 ⊆ 𝐵 ▶ (𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 𝐵) )
8:7:	⊢ ( 𝐴 ⊆ 𝐵 ▶ ∀𝑥(𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 𝐵) )
9:8:	⊢ ( 𝐴 ⊆ 𝐵 ▶ 𝒫 𝐴 ⊆ 𝒫 𝐵 )
qed:9:	⊢ (𝐴 ⊆ 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵)

(𝐴 ⊆ 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵)

Theorem

sspwimpcf 44916

If a class is a subclass of another class, then its power class is a subclass of that other class's power class. Left-to-right implication of Exercise 18 of [TakeutiZaring] p. 18. sspwimpcf 44916, using conventional notation, was translated from its virtual deduction form, sspwimpcfVD 44917, using a translation program. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.)

(𝐴 ⊆ 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵)

Theorem

sspwimpcfVD 44917

The following User's Proof is a Virtual Deduction proof (see wvd1 44566) using conjunction-form virtual hypothesis collections. It was completed automatically by a tools program which would invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. sspwimpcf 44916 is sspwimpcfVD 44917 without virtual deductions and was derived from sspwimpcfVD 44917. The version of completeusersproof.cmd used is capable of only generating conjunction-form unification theorems, not unification deductions. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.)

1::	⊢ ( 𝐴 ⊆ 𝐵 ▶ 𝐴 ⊆ 𝐵 )
2::	⊢ ( ........... 𝑥 ∈ 𝒫 𝐴 ▶ 𝑥 ∈ 𝒫 𝐴 )
3:2:	⊢ ( ........... 𝑥 ∈ 𝒫 𝐴 ▶ 𝑥 ⊆ 𝐴 )
4:3,1:	⊢ ( ( 𝐴 ⊆ 𝐵 , 𝑥 ∈ 𝒫 𝐴 ) ▶ 𝑥 ⊆ 𝐵 )
5::	⊢ 𝑥 ∈ V
6:4,5:	⊢ ( ( 𝐴 ⊆ 𝐵 , 𝑥 ∈ 𝒫 𝐴 ) ▶ 𝑥 ∈ 𝒫 𝐵 )
7:6:	⊢ ( 𝐴 ⊆ 𝐵 ▶ (𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 𝐵) )
8:7:	⊢ ( 𝐴 ⊆ 𝐵 ▶ ∀𝑥(𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 𝐵) )
9:8:	⊢ ( 𝐴 ⊆ 𝐵 ▶ 𝒫 𝐴 ⊆ 𝒫 𝐵 )
qed:9:	⊢ (𝐴 ⊆ 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵)

(𝐴 ⊆ 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵)

Theorem

suctrALTcf 44918

The successor of a transitive class is transitive. suctrALTcf 44918, using conventional notation, was translated from virtual deduction form, suctrALTcfVD 44919, using a translation program. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.)

(Tr 𝐴 → Tr suc 𝐴)

Theorem

suctrALTcfVD 44919

The following User's Proof is a Virtual Deduction proof (see wvd1 44566) using conjunction-form virtual hypothesis collections. The conjunction-form version of completeusersproof.cmd. It allows the User to avoid superflous virtual hypotheses. This proof was completed automatically by a tools program which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. suctrALTcf 44918 is suctrALTcfVD 44919 without virtual deductions and was derived automatically from suctrALTcfVD 44919. The version of completeusersproof.cmd used is capable of only generating conjunction-form unification theorems, not unification deductions. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.)

1::	⊢ ( Tr 𝐴 ▶ Tr 𝐴 )
2::	⊢ ( ......... (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) ▶ (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) )
3:2:	⊢ ( ......... (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) ▶ 𝑧 ∈ 𝑦 )
4::	⊢ ( ................................... ....... 𝑦 ∈ 𝐴 ▶ 𝑦 ∈ 𝐴 )
5:1,3,4:	⊢ ( ( Tr 𝐴 , (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) , 𝑦 ∈ 𝐴 ) ▶ 𝑧 ∈ 𝐴 )
6::	⊢ 𝐴 ⊆ suc 𝐴
7:5,6:	⊢ ( ( Tr 𝐴 , (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) , 𝑦 ∈ 𝐴 ) ▶ 𝑧 ∈ suc 𝐴 )
8:7:	⊢ ( ( Tr 𝐴 , (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) ) ▶ (𝑦 ∈ 𝐴 → 𝑧 ∈ suc 𝐴) )
9::	⊢ ( ................................... ...... 𝑦 = 𝐴 ▶ 𝑦 = 𝐴 )
10:3,9:	⊢ ( ........ ( (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴), 𝑦 = 𝐴 ) ▶ 𝑧 ∈ 𝐴 )
11:10,6:	⊢ ( ........ ( (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴), 𝑦 = 𝐴 ) ▶ 𝑧 ∈ suc 𝐴 )
12:11:	⊢ ( .......... (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) ▶ (𝑦 = 𝐴 → 𝑧 ∈ suc 𝐴) )
13:2:	⊢ ( .......... (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) ▶ 𝑦 ∈ suc 𝐴 )
14:13:	⊢ ( .......... (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) ▶ (𝑦 ∈ 𝐴 ∨ 𝑦 = 𝐴) )
15:8,12,14:	⊢ ( ( Tr 𝐴 , (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) ) ▶ 𝑧 ∈ suc 𝐴 )
16:15:	⊢ ( Tr 𝐴 ▶ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → 𝑧 ∈ suc 𝐴) )
17:16:	⊢ ( Tr 𝐴 ▶ ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → 𝑧 ∈ suc 𝐴) )
18:17:	⊢ ( Tr 𝐴 ▶ Tr suc 𝐴 )
qed:18:	⊢ (Tr 𝐴 → Tr suc 𝐴)

(Tr 𝐴 → Tr suc 𝐴)

21.41.10 Theorems with a VD proof in conventional notation derived from a VD proof

Theorem

suctrALT3 44920

The successor of a transitive class is transitive. suctrALT3 44920 is the completed proof in conventional notation of the Virtual Deduction proof https://us.metamath.org/other/completeusersproof/suctralt3vd.html 44920. It was completed manually. The potential for automated derivation from the VD proof exists. See wvd1 44566 for a description of Virtual Deduction. Some sub-theorems of the proof were completed using a unification deduction (e.g., the sub-theorem whose assertion is step 19 used jaoded 44563). Unification deductions employ Mario Carneiro's metavariable concept. Some sub-theorems were completed using a unification theorem (e.g., the sub-theorem whose assertion is step 24 used dftr2 5219) . (Contributed by Alan Sare, 3-Dec-2015.) (Proof modification is discouraged.) (New usage is discouraged.)

(Tr 𝐴 → Tr suc 𝐴)

Theorem

sspwimpALT 44921

If a class is a subclass of another class, then its power class is a subclass of that other class's power class. Left-to-right implication of Exercise 18 of [TakeutiZaring] p. 18. sspwimpALT 44921 is the completed proof in conventional notation of the Virtual Deduction proof https://us.metamath.org/other/completeusersproof/sspwimpaltvd.html 44921. It was completed manually. The potential for automated derivation from the VD proof exists. See wvd1 44566 for a description of Virtual Deduction. Some sub-theorems of the proof were completed using a unification deduction (e.g., the sub-theorem whose assertion is step 9 used elpwgded 44561). Unification deductions employ Mario Carneiro's metavariable concept. Some sub-theorems were completed using a unification theorem (e.g., the sub-theorem whose assertion is step 5 used elpwi 4573). (Contributed by Alan Sare, 3-Dec-2015.) (Proof modification is discouraged.) (New usage is discouraged.)

(𝐴 ⊆ 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵)

Theorem

unisnALT 44922

A set equals the union of its singleton. Theorem 8.2 of [Quine] p. 53. The User manually input on a mmj2 Proof Worksheet, without labels, all steps of unisnALT 44922 except 1, 11, 15, 21, and 30. With execution of the mmj2 unification command, mmj2 could find labels for all steps except for 2, 12, 16, 22, and 31 (and the then non-existing steps 1, 11, 15, 21, and 30). mmj2 could not find reference theorems for those five steps because the hypothesis field of each of these steps was empty and none of those steps unifies with a theorem in set.mm. Each of these five steps is a semantic variation of a theorem in set.mm and is 2-step provable. mmj2 does not have the ability to automatically generate the semantic variation in set.mm of a theorem in a mmj2 Proof Worksheet unless the theorem in the Proof Worksheet is labeled with a 1-hypothesis deduction whose hypothesis is a theorem in set.mm which unifies with the theorem in the Proof Worksheet. The stepprover.c program, which invokes mmj2, has this capability. stepprover.c automatically generated steps 1, 11, 15, 21, and 30, labeled all steps, and generated the RPN proof of unisnALT 44922. Roughly speaking, stepprover.c added to the Proof Worksheet a labeled duplicate step of each non-unifying theorem for each label in a text file, labels.txt, containing a list of labels provided by the User. Upon mmj2 unification, stepprover.c identified a label for each of the five theorems which 2-step proves it. For unisnALT 44922, the label list is a list of all 1-hypothesis propositional calculus deductions in set.mm. stepproverp.c is the same as stepprover.c except that it intermittently pauses during execution, allowing the User to observe the changes to a text file caused by the execution of particular statements of the program. (Contributed by Alan Sare, 19-Aug-2016.) (Proof modification is discouraged.) (New usage is discouraged.)

𝐴 ∈ V ⇒ ∪ {𝐴} = 𝐴

21.41.11 Theorems with a proof in conventional notation derived from a VD proof

Theorems with a proof in conventional notation automatically derived by completeusersproof.c from a Virtual Deduction User's Proof.

Theorem

notnotrALT2 44923

Converse of double negation. Theorem *2.14 of [WhiteheadRussell] p. 102. Proof derived by completeusersproof.c from User's Proof in VirtualDeductionProofs.txt. (Contributed by Alan Sare, 11-Sep-2016.) (Proof modification is discouraged.) (New usage is discouraged.)

(¬ ¬ 𝜑 → 𝜑)

Theorem

sspwimpALT2 44924

If a class is a subclass of another class, then its power class is a subclass of that other class's power class. Left-to-right implication of Exercise 18 of [TakeutiZaring] p. 18. Proof derived by completeusersproof.c from User's Proof in VirtualDeductionProofs.txt. The User's Proof in html format is displayed in https://us.metamath.org/other/completeusersproof/sspwimpaltvd.html. (Contributed by Alan Sare, 11-Sep-2016.) (Proof modification is discouraged.) (New usage is discouraged.)

(𝐴 ⊆ 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵)

Theorem

e2ebindALT 44925

Absorption of an existential quantifier of a double existential quantifier of non-distinct variables. The proof is derived by completeusersproof.c from User's Proof in VirtualDeductionProofs.txt. The User's Proof in html format is displayed in e2ebindVD 44908. (Contributed by Alan Sare, 11-Sep-2016.) (Proof modification is discouraged.) (New usage is discouraged.)

(∀𝑥 𝑥 = 𝑦 → (∃𝑥∃𝑦𝜑 ↔ ∃𝑦𝜑))

Theorem

ax6e2ndALT 44926*

If at least two sets exist (dtru 5399), then the same is true expressed in an alternate form similar to the form of ax6e 2382. The proof is derived by completeusersproof.c from User's Proof in VirtualDeductionProofs.txt. The User's Proof in html format is displayed in ax6e2ndVD 44904. (Contributed by Alan Sare, 11-Sep-2016.) (Proof modification is discouraged.) (New usage is discouraged.)

(¬ ∀𝑥 𝑥 = 𝑦 → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))

Theorem

ax6e2ndeqALT 44927*

"At least two sets exist" expressed in the form of dtru 5399 is logically equivalent to the same expressed in a form similar to ax6e 2382 if dtru 5399 is false implies 𝑢 = 𝑣. Proof derived by completeusersproof.c from User's Proof in VirtualDeductionProofs.txt. The User's Proof in html format is displayed in ax6e2ndeqVD 44905. (Contributed by Alan Sare, 11-Sep-2016.) (Proof modification is discouraged.) (New usage is discouraged.)

((¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣) ↔ ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))

Theorem

2sb5ndALT 44928*

Equivalence for double substitution 2sb5 2278 without distinct 𝑥, 𝑦 requirement. 2sb5nd 44557 is derived from 2sb5ndVD 44906. The proof is derived by completeusersproof.c from User's Proof in VirtualDeductionProofs.txt. The User's Proof in html format is displayed in 2sb5ndVD 44906. (Contributed by Alan Sare, 19-Sep-2016.) (Proof modification is discouraged.) (New usage is discouraged.)

((¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣) → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ↔ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑)))

Theorem

chordthmALT 44929*

The intersecting chords theorem. If points A, B, C, and D lie on a circle (with center Q, say), and the point P is on the interior of the segments AB and CD, then the two products of lengths PA · PB and PC · PD are equal. The Euclidean plane is identified with the complex plane, and the fact that P is on AB and on CD is expressed by the hypothesis that the angles APB and CPD are equal to π. The result is proven by using chordthmlem5 26753 twice to show that PA · PB and PC · PD both equal BQ ² − PQ ² . This is similar to the proof of the theorem given in Euclid's Elements, where it is Proposition III.35. Proven by David Moews on 28-Feb-2017 as chordthm 26754. https://us.metamath.org/other/completeusersproof/chordthmaltvd.html 26754 is a Virtual Deduction User's Proof transcription of chordthm 26754. That VD User's Proof was input into completeusersproof, automatically generating this chordthmALT 44929 Metamath proof. (Contributed by Alan Sare, 19-Sep-2017.) (Proof modification is discouraged.) (New usage is discouraged.)

𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (ℑ‘(log‘(𝑦 / 𝑥)))) & (𝜑 → 𝐴 ∈ ℂ) & (𝜑 → 𝐵 ∈ ℂ) & (𝜑 → 𝐶 ∈ ℂ) & (𝜑 → 𝐷 ∈ ℂ) & (𝜑 → 𝑃 ∈ ℂ) & (𝜑 → 𝐴 ≠ 𝑃) & (𝜑 → 𝐵 ≠ 𝑃) & (𝜑 → 𝐶 ≠ 𝑃) & (𝜑 → 𝐷 ≠ 𝑃) & (𝜑 → ((𝐴 − 𝑃)𝐹(𝐵 − 𝑃)) = π) & (𝜑 → ((𝐶 − 𝑃)𝐹(𝐷 − 𝑃)) = π) & (𝜑 → 𝑄 ∈ ℂ) & (𝜑 → (abs‘(𝐴 − 𝑄)) = (abs‘(𝐵 − 𝑄))) & (𝜑 → (abs‘(𝐴 − 𝑄)) = (abs‘(𝐶 − 𝑄))) & (𝜑 → (abs‘(𝐴 − 𝑄)) = (abs‘(𝐷 − 𝑄))) ⇒ (𝜑 → ((abs‘(𝑃 − 𝐴)) · (abs‘(𝑃 − 𝐵))) = ((abs‘(𝑃 − 𝐶)) · (abs‘(𝑃 − 𝐷))))

Theorem

isosctrlem1ALT 44930

Lemma for isosctr 26738. This proof was automatically derived by completeusersproof from its Virtual Deduction proof counterpart https://us.metamath.org/other/completeusersproof/isosctrlem1altvd.html 26738. As it is verified by the Metamath program, isosctrlem1ALT 44930 verifies https://us.metamath.org/other/completeusersproof/isosctrlem1altvd.html 44930. (Contributed by Alan Sare, 22-Apr-2018.) (Proof modification is discouraged.) (New usage is discouraged.)

((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) → (ℑ‘(log‘(1 − 𝐴))) ≠ π)

Theorem

iunconnlem2 44931*

The indexed union of connected overlapping subspaces sharing a common point is connected. This proof was automatically derived by completeusersproof from its Virtual Deduction proof counterpart https://us.metamath.org/other/completeusersproof/iunconlem2vd.html. As it is verified by the Metamath program, iunconnlem2 44931 verifies https://us.metamath.org/other/completeusersproof/iunconlem2vd.html 44931. (Contributed by Alan Sare, 22-Apr-2018.) (Proof modification is discouraged.) (New usage is discouraged.)

(𝜓 ↔ ((((((𝜑 ∧ 𝑢 ∈ 𝐽) ∧ 𝑣 ∈ 𝐽) ∧ (𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵) ≠ ∅) ∧ (𝑣 ∩ ∪ 𝑘 ∈ 𝐴 𝐵) ≠ ∅) ∧ (𝑢 ∩ 𝑣) ⊆ (𝑋 ∖ ∪ 𝑘 ∈ 𝐴 𝐵)) ∧ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ (𝑢 ∪ 𝑣))) & (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ⊆ 𝑋) & ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑃 ∈ 𝐵) & ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐽 ↾_t 𝐵) ∈ Conn) ⇒ (𝜑 → (𝐽 ↾_t ∪ 𝑘 ∈ 𝐴 𝐵) ∈ Conn)

Theorem

iunconnALT 44932*

The indexed union of connected overlapping subspaces sharing a common point is connected. This proof was automatically derived by completeusersproof from its Virtual Deduction proof counterpart https://us.metamath.org/other/completeusersproof/iunconaltvd.html. As it is verified by the Metamath program, iunconnALT 44932 verifies https://us.metamath.org/other/completeusersproof/iunconaltvd.html 44932. (Contributed by Alan Sare, 22-Apr-2018.) (Proof modification is discouraged.) (New usage is discouraged.)

(𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ⊆ 𝑋) & ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑃 ∈ 𝐵) & ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐽 ↾_t 𝐵) ∈ Conn) ⇒ (𝜑 → (𝐽 ↾_t ∪ 𝑘 ∈ 𝐴 𝐵) ∈ Conn)

Theorem

sineq0ALT 44933

A complex number whose sine is zero is an integer multiple of π. The Virtual Deduction form of the proof is https://us.metamath.org/other/completeusersproof/sineq0altvd.html. The Metamath form of the proof is sineq0ALT 44933. The Virtual Deduction proof is based on Mario Carneiro's revision of Norm Megill's proof of sineq0 26440. The Virtual Deduction proof is verified by automatically transforming it into the Metamath form of the proof using completeusersproof, which is verified by the Metamath program. The proof of https://us.metamath.org/other/completeusersproof/sineq0altro.html 26440 is a form of the completed proof which preserves the Virtual Deduction proof's step numbers and their ordering. (Contributed by Alan Sare, 13-Jun-2018.) (Proof modification is discouraged.) (New usage is discouraged.)

(𝐴 ∈ ℂ → ((sin‘𝐴) = 0 ↔ (𝐴 / π) ∈ ℤ))

21.42 Mathbox for Eric Schmidt

21.42.1 Miscellany

Theorem

rspesbcd 44934*

Restricted quantifier version of spesbcd 3849. (Contributed by Eric Schmidt, 29-Sep-2025.)

(𝜑 → 𝐴 ∈ 𝐵) & (𝜑 → [𝐴 / 𝑥]𝜓) ⇒ (𝜑 → ∃𝑥 ∈ 𝐵 𝜓)

Theorem

rext0 44935*

Nonempty existential quantification of a theorem is true. (Contributed by Eric Schmidt, 19-Oct-2025.)

𝜑 ⇒ (∃𝑥 ∈ 𝐴 𝜑 ↔ 𝐴 ≠ ∅)

21.42.2 Study of dfbi1ALT

Theorem

dfbi1ALTa 44936

Version of dfbi1ALT 214 using ⊤ for step 2 and shortened using a1i 11, a2i 14, and con4i 114. (Contributed by Eric Schmidt, 22-Oct-2025.) (New usage is discouraged.) (Proof modification is discouraged.)

((𝜑 ↔ 𝜓) ↔ ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)))

Theorem

simprimi 44937

Inference associated with simprim 166. Proved exactly as step 11 is obtained from step 4 in dfbi1ALTa 44936. (Contributed by Eric Schmidt, 22-Oct-2025.) (New usage is discouraged.) (Proof modification is discouraged.)

¬ (𝜑 → ¬ 𝜓) ⇒ 𝜓

Theorem

dfbi1ALTb 44938

Further shorten dfbi1ALTa 44936 using simprimi 44937. (Contributed by Eric Schmidt, 22-Oct-2025.) (New usage is discouraged.) (Proof modification is discouraged.)

((𝜑 ↔ 𝜓) ↔ ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)))

21.42.3 Relation-preserving functions

Syntax

wrelp 44939

Extend the definition of a wff to include the relation-preserving property. (Contributed by Eric Schmidt, 11-Oct-2025.)

wff 𝐻 RelPres 𝑅, 𝑆(𝐴, 𝐵)

Definition

df-relp 44940*

Define the relation-preserving predicate. This is a viable notion of "homomorphism" corresponding to df-isom 6523. (Contributed by Eric Schmidt, 11-Oct-2025.)

(𝐻 RelPres 𝑅, 𝑆(𝐴, 𝐵) ↔ (𝐻:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦))))

Theorem

relpeq1 44941