P. 451 of Theorem List - Metamath Proof Explorer

Type

Label

Description

Statement

Theorem

onfrALTlem5VD 45001*

Virtual deduction proof of onfrALTlem5 44659. 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. onfrALTlem5 44659 is onfrALTlem5VD 45001 without virtual deductions and was automatically derived from onfrALTlem5VD 45001.

1::	⊢ 𝑎 ∈ V
2:1:	⊢ (𝑎 ∩ 𝑥) ∈ V
3:2:	⊢ ([(𝑎 ∩ 𝑥) / 𝑏]𝑏 = ∅ ↔ (𝑎 ∩ 𝑥) = ∅)
4:3:	⊢ (¬ [(𝑎 ∩ 𝑥) / 𝑏]𝑏 = ∅ ↔ ¬ (𝑎 ∩ 𝑥) = ∅)
5::	⊢ ((𝑎 ∩ 𝑥) ≠ ∅ ↔ ¬ (𝑎 ∩ 𝑥 ) = ∅)
6:4,5:	⊢ (¬ [(𝑎 ∩ 𝑥) / 𝑏]𝑏 = ∅ ↔ (𝑎 ∩ 𝑥) ≠ ∅)
7:2:	⊢ (¬ [(𝑎 ∩ 𝑥) / 𝑏]𝑏 = ∅ ↔ [(𝑎 ∩ 𝑥) / 𝑏]¬ 𝑏 = ∅)
8::	⊢ (𝑏 ≠ ∅ ↔ ¬ 𝑏 = ∅)
9:8:	⊢ ∀𝑏(𝑏 ≠ ∅ ↔ ¬ 𝑏 = ∅)
10:2,9:	⊢ ([(𝑎 ∩ 𝑥) / 𝑏]𝑏 ≠ ∅ ↔ [(𝑎 ∩ 𝑥) / 𝑏]¬ 𝑏 = ∅)
11:7,10:	⊢ (¬ [(𝑎 ∩ 𝑥) / 𝑏]𝑏 = ∅ ↔ [(𝑎 ∩ 𝑥) / 𝑏]𝑏 ≠ ∅)
12:6,11:	⊢ ([(𝑎 ∩ 𝑥) / 𝑏]𝑏 ≠ ∅ ↔ ( 𝑎 ∩ 𝑥) ≠ ∅)
13:2:	⊢ ([(𝑎 ∩ 𝑥) / 𝑏]𝑏 ⊆ (𝑎 ∩ 𝑥 ) ↔ (𝑎 ∩ 𝑥) ⊆ (𝑎 ∩ 𝑥))
14:12,13:	⊢ (([(𝑎 ∩ 𝑥) / 𝑏]𝑏 ⊆ (𝑎 ∩ 𝑥) ∧ [(𝑎 ∩ 𝑥) / 𝑏]𝑏 ≠ ∅) ↔ ((𝑎 ∩ 𝑥) ⊆ (𝑎 ∩ 𝑥) ∧ (𝑎 ∩ 𝑥) ≠ ∅))
15:2:	⊢ ([(𝑎 ∩ 𝑥) / 𝑏](𝑏 ⊆ (𝑎 ∩ 𝑥) ∧ 𝑏 ≠ ∅) ↔ ([(𝑎 ∩ 𝑥) / 𝑏]𝑏 ⊆ (𝑎 ∩ 𝑥) ∧ [(𝑎 ∩ 𝑥) / 𝑏]𝑏 ≠ ∅))
16:15,14:	⊢ ([(𝑎 ∩ 𝑥) / 𝑏](𝑏 ⊆ (𝑎 ∩ 𝑥) ∧ 𝑏 ≠ ∅) ↔ ((𝑎 ∩ 𝑥) ⊆ (𝑎 ∩ 𝑥) ∧ (𝑎 ∩ 𝑥) ≠ ∅))
17:2:	⊢ ⦋(𝑎 ∩ 𝑥) / 𝑏⦌(𝑏 ∩ 𝑦) = ( ⦋(𝑎 ∩ 𝑥) / 𝑏⦌𝑏 ∩ ⦋(𝑎 ∩ 𝑥) / 𝑏⦌𝑦)
18:2:	⊢ ⦋(𝑎 ∩ 𝑥) / 𝑏⦌𝑏 = (𝑎 ∩ 𝑥)
19:2:	⊢ ⦋(𝑎 ∩ 𝑥) / 𝑏⦌𝑦 = 𝑦
20:18,19:	⊢ (⦋(𝑎 ∩ 𝑥) / 𝑏⦌𝑏 ∩ ⦋(𝑎 ∩ 𝑥) / 𝑏⦌𝑦) = ((𝑎 ∩ 𝑥) ∩ 𝑦)
21:17,20:	⊢ ⦋(𝑎 ∩ 𝑥) / 𝑏⦌(𝑏 ∩ 𝑦) = (( 𝑎 ∩ 𝑥) ∩ 𝑦)
22:2:	⊢ ([(𝑎 ∩ 𝑥) / 𝑏](𝑏 ∩ 𝑦) = ∅ ↔ ⦋(𝑎 ∩ 𝑥) / 𝑏⦌(𝑏 ∩ 𝑦) = ⦋(𝑎 ∩ 𝑥) / 𝑏⦌ ∅)
23:2:	⊢ ⦋(𝑎 ∩ 𝑥) / 𝑏⦌∅ = ∅
24:21,23:	⊢ (⦋(𝑎 ∩ 𝑥) / 𝑏⦌(𝑏 ∩ 𝑦) = ⦋(𝑎 ∩ 𝑥) / 𝑏⦌∅ ↔ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅)
25:22,24:	⊢ ([(𝑎 ∩ 𝑥) / 𝑏](𝑏 ∩ 𝑦) = ∅ ↔ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅)
26:2:	⊢ ([(𝑎 ∩ 𝑥) / 𝑏]𝑦 ∈ 𝑏 ↔ 𝑦 ∈ (𝑎 ∩ 𝑥))
27:25,26:	⊢ (([(𝑎 ∩ 𝑥) / 𝑏]𝑦 ∈ 𝑏 ∧ [ (𝑎 ∩ 𝑥) / 𝑏](𝑏 ∩ 𝑦) = ∅) ↔ (𝑦 ∈ (𝑎 ∩ 𝑥) ∧ (( 𝑎 ∩ 𝑥) ∩ 𝑦) = ∅))
28:2:	⊢ ([(𝑎 ∩ 𝑥) / 𝑏](𝑦 ∈ 𝑏 ∧ (𝑏 ∩ 𝑦) = ∅) ↔ ([(𝑎 ∩ 𝑥) / 𝑏]𝑦 ∈ 𝑏 ∧ [(𝑎 ∩ 𝑥) / 𝑏](𝑏 ∩ 𝑦) = ∅))
29:27,28:	⊢ ([(𝑎 ∩ 𝑥) / 𝑏](𝑦 ∈ 𝑏 ∧ (𝑏 ∩ 𝑦) = ∅) ↔ (𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅))
30:29:	⊢ ∀𝑦([(𝑎 ∩ 𝑥) / 𝑏](𝑦 ∈ 𝑏 ∧ (𝑏 ∩ 𝑦) = ∅) ↔ (𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅))
31:30:	⊢ (∃𝑦[(𝑎 ∩ 𝑥) / 𝑏](𝑦 ∈ 𝑏 ∧ (𝑏 ∩ 𝑦) = ∅) ↔ ∃𝑦(𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅))
32::	⊢ (∃𝑦 ∈ (𝑎 ∩ 𝑥)((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅ ↔ ∃𝑦(𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅ ))
33:31,32:	⊢ (∃𝑦[(𝑎 ∩ 𝑥) / 𝑏](𝑦 ∈ 𝑏 ∧ (𝑏 ∩ 𝑦) = ∅) ↔ ∃𝑦 ∈ (𝑎 ∩ 𝑥)((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅)
34:2:	⊢ (∃𝑦[(𝑎 ∩ 𝑥) / 𝑏](𝑦 ∈ 𝑏 ∧ (𝑏 ∩ 𝑦) = ∅) ↔ [(𝑎 ∩ 𝑥) / 𝑏]∃𝑦(𝑦 ∈ 𝑏 ∧ ( 𝑏 ∩ 𝑦) = ∅))
35:33,34:	⊢ ([(𝑎 ∩ 𝑥) / 𝑏]∃𝑦(𝑦 ∈ 𝑏 ∧ (𝑏 ∩ 𝑦) = ∅) ↔ ∃𝑦 ∈ (𝑎 ∩ 𝑥)((𝑎 ∩ 𝑥) ∩ 𝑦 ) = ∅)
36::	⊢ (∃𝑦 ∈ 𝑏(𝑏 ∩ 𝑦) = ∅ ↔ ∃𝑦 (𝑦 ∈ 𝑏 ∧ (𝑏 ∩ 𝑦) = ∅))
37:36:	⊢ ∀𝑏(∃𝑦 ∈ 𝑏(𝑏 ∩ 𝑦) = ∅ ↔ ∃𝑦(𝑦 ∈ 𝑏 ∧ (𝑏 ∩ 𝑦) = ∅))
38:2,37:	⊢ ([(𝑎 ∩ 𝑥) / 𝑏]∃𝑦 ∈ 𝑏(𝑏 ∩ 𝑦) = ∅ ↔ [(𝑎 ∩ 𝑥) / 𝑏]∃𝑦(𝑦 ∈ 𝑏 ∧ (𝑏 ∩ 𝑦) = ∅))
39:35,38:	⊢ ([(𝑎 ∩ 𝑥) / 𝑏]∃𝑦 ∈ 𝑏(𝑏 ∩ 𝑦) = ∅ ↔ ∃𝑦 ∈ (𝑎 ∩ 𝑥)((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅)
40:16,39:	⊢ (([(𝑎 ∩ 𝑥) / 𝑏](𝑏 ⊆ (𝑎 ∩ 𝑥) ∧ 𝑏 ≠ ∅) → [(𝑎 ∩ 𝑥) / 𝑏]∃𝑦 ∈ 𝑏(𝑏 ∩ 𝑦) = ∅) ↔ (((𝑎 ∩ 𝑥) ⊆ (𝑎 ∩ 𝑥) ∧ (𝑎 ∩ 𝑥) ≠ ∅) → ∃𝑦 ∈ (𝑎 ∩ 𝑥)((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅))
41:2:	⊢ ([(𝑎 ∩ 𝑥) / 𝑏]((𝑏 ⊆ (𝑎 ∩ 𝑥) ∧ 𝑏 ≠ ∅) → ∃𝑦 ∈ 𝑏(𝑏 ∩ 𝑦) = ∅) ↔ ([(𝑎 ∩ 𝑥) / 𝑏](𝑏 ⊆ (𝑎 ∩ 𝑥) ∧ 𝑏 ≠ ∅) → [(𝑎 ∩ 𝑥) / 𝑏]∃𝑦 ∈ 𝑏(𝑏 ∩ 𝑦) = ∅))
qed:40,41:	⊢ ([(𝑎 ∩ 𝑥) / 𝑏]((𝑏 ⊆ (𝑎 ∩ 𝑥) ∧ 𝑏 ≠ ∅) → ∃𝑦 ∈ 𝑏(𝑏 ∩ 𝑦) = ∅) ↔ (((𝑎 ∩ 𝑥) ⊆ (𝑎 ∩ 𝑥) ∧ (𝑎 ∩ 𝑥) ≠ ∅) → ∃𝑦 ∈ (𝑎 ∩ 𝑥 )((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅))

(Contributed by Alan Sare, 22-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ ([(𝑎 ∩ 𝑥) / 𝑏]((𝑏 ⊆ (𝑎 ∩ 𝑥) ∧ 𝑏 ≠ ∅) → ∃𝑦 ∈ 𝑏 (𝑏 ∩ 𝑦) = ∅) ↔ (((𝑎 ∩ 𝑥) ⊆ (𝑎 ∩ 𝑥) ∧ (𝑎 ∩ 𝑥) ≠ ∅) → ∃𝑦 ∈ (𝑎 ∩ 𝑥)((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅))

Theorem

onfrALTlem4VD 45002*

Virtual deduction proof of onfrALTlem4 44660. 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. onfrALTlem4 44660 is onfrALTlem4VD 45002 without virtual deductions and was automatically derived from onfrALTlem4VD 45002.

1::	⊢ 𝑦 ∈ V
2:1:	⊢ ([𝑦 / 𝑥](𝑎 ∩ 𝑥) = ∅ ↔ ⦋ 𝑦 / 𝑥⦌(𝑎 ∩ 𝑥) = ⦋𝑦 / 𝑥⦌∅)
3:1:	⊢ ⦋𝑦 / 𝑥⦌(𝑎 ∩ 𝑥) = (⦋𝑦 / 𝑥⦌ 𝑎 ∩ ⦋𝑦 / 𝑥⦌𝑥)
4:1:	⊢ ⦋𝑦 / 𝑥⦌𝑎 = 𝑎
5:1:	⊢ ⦋𝑦 / 𝑥⦌𝑥 = 𝑦
6:4,5:	⊢ (⦋𝑦 / 𝑥⦌𝑎 ∩ ⦋𝑦 / 𝑥⦌𝑥) = ( 𝑎 ∩ 𝑦)
7:3,6:	⊢ ⦋𝑦 / 𝑥⦌(𝑎 ∩ 𝑥) = (𝑎 ∩ 𝑦)
8:1:	⊢ ⦋𝑦 / 𝑥⦌∅ = ∅
9:7,8:	⊢ (⦋𝑦 / 𝑥⦌(𝑎 ∩ 𝑥) = ⦋𝑦 / 𝑥⦌ ∅ ↔ (𝑎 ∩ 𝑦) = ∅)
10:2,9:	⊢ ([𝑦 / 𝑥](𝑎 ∩ 𝑥) = ∅ ↔ (𝑎 ∩ 𝑦) = ∅)
11:1:	⊢ ([𝑦 / 𝑥]𝑥 ∈ 𝑎 ↔ 𝑦 ∈ 𝑎)
12:11,10:	⊢ (([𝑦 / 𝑥]𝑥 ∈ 𝑎 ∧ [𝑦 / 𝑥]( 𝑎 ∩ 𝑥) = ∅) ↔ (𝑦 ∈ 𝑎 ∧ (𝑎 ∩ 𝑦) = ∅))
13:1:	⊢ ([𝑦 / 𝑥](𝑥 ∈ 𝑎 ∧ (𝑎 ∩ 𝑥) = ∅) ↔ ([𝑦 / 𝑥]𝑥 ∈ 𝑎 ∧ [𝑦 / 𝑥](𝑎 ∩ 𝑥) = ∅))
qed:13,12:	⊢ ([𝑦 / 𝑥](𝑥 ∈ 𝑎 ∧ (𝑎 ∩ 𝑥) = ∅) ↔ (𝑦 ∈ 𝑎 ∧ (𝑎 ∩ 𝑦) = ∅))

(Contributed by Alan Sare, 22-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ ([𝑦 / 𝑥](𝑥 ∈ 𝑎 ∧ (𝑎 ∩ 𝑥) = ∅) ↔ (𝑦 ∈ 𝑎 ∧ (𝑎 ∩ 𝑦) = ∅))

Theorem

onfrALTlem3VD 45003*

Virtual deduction proof of onfrALTlem3 44661. 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. onfrALTlem3 44661 is onfrALTlem3VD 45003 without virtual deductions and was automatically derived from onfrALTlem3VD 45003.

1::	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ▶   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   )
2::	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   )
3:2:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   𝑥 ∈ 𝑎   )
4:1:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ▶   𝑎 ⊆ On   )
5:3,4:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   𝑥 ∈ On   )
6:5:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   Ord 𝑥   )
7:6:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶    E We 𝑥   )
8::	⊢ (𝑎 ∩ 𝑥) ⊆ 𝑥
9:7,8:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶    E We (𝑎 ∩ 𝑥)   )
10:9:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶    E Fr (𝑎 ∩ 𝑥)   )
11:10:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   ∀𝑏((𝑏 ⊆ (𝑎 ∩ 𝑥) ∧ 𝑏 ≠ ∅) → ∃𝑦 ∈ 𝑏(𝑏 ∩ 𝑦) = ∅)   )
12::	⊢ 𝑥 ∈ V
13:12,8:	⊢ (𝑎 ∩ 𝑥) ∈ V
14:13,11:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   [(𝑎 ∩ 𝑥) / 𝑏]((𝑏 ⊆ (𝑎 ∩ 𝑥) ∧ 𝑏 ≠ ∅) → ∃𝑦 ∈ 𝑏(𝑏 ∩ 𝑦) = ∅)   )
15::	⊢ ([(𝑎 ∩ 𝑥) / 𝑏]((𝑏 ⊆ (𝑎 ∩ 𝑥) ∧ 𝑏 ≠ ∅) → ∃𝑦 ∈ 𝑏(𝑏 ∩ 𝑦) = ∅) ↔ (((𝑎 ∩ 𝑥) ⊆ (𝑎 ∩ 𝑥) ∧ (𝑎 ∩ 𝑥) ≠ ∅) → ∃𝑦 ∈ (𝑎 ∩ 𝑥)( (𝑎 ∩ 𝑥) ∩ 𝑦) = ∅))
16:14,15:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   (((𝑎 ∩ 𝑥) ⊆ (𝑎 ∩ 𝑥) ∧ ( 𝑎 ∩ 𝑥) ≠ ∅) → ∃𝑦 ∈ (𝑎 ∩ 𝑥)((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅)   )
17::	⊢ (𝑎 ∩ 𝑥) ⊆ (𝑎 ∩ 𝑥)
18:2:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   ¬ (𝑎 ∩ 𝑥) = ∅   )
19:18:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   (𝑎 ∩ 𝑥) ≠ ∅   )
20:17,19:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   ((𝑎 ∩ 𝑥) ⊆ (𝑎 ∩ 𝑥) ∧ (𝑎 ∩ 𝑥) ≠ ∅)   )
qed:16,20:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   ∃𝑦 ∈ (𝑎 ∩ 𝑥)((𝑎 ∩ 𝑥) ∩ 𝑦 ) = ∅   )

(Contributed by Alan Sare, 22-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   ∃𝑦 ∈ (𝑎 ∩ 𝑥)((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅   )

Theorem

simplbi2comtVD 45004

Virtual deduction proof of simplbi2comt 501. 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. simplbi2comt 501 is simplbi2comtVD 45004 without virtual deductions and was automatically derived from simplbi2comtVD 45004.

1::	⊢ (   (𝜑 ↔ (𝜓 ∧ 𝜒))   ▶   (𝜑 ↔ ( 𝜓 ∧ 𝜒))   )
2:1:	⊢ (   (𝜑 ↔ (𝜓 ∧ 𝜒))   ▶   ((𝜓 ∧ 𝜒 ) → 𝜑)   )
3:2:	⊢ (   (𝜑 ↔ (𝜓 ∧ 𝜒))   ▶   (𝜓 → (𝜒 → 𝜑))   )
4:3:	⊢ (   (𝜑 ↔ (𝜓 ∧ 𝜒))   ▶   (𝜒 → (𝜓 → 𝜑))   )
qed:4:	⊢ ((𝜑 ↔ (𝜓 ∧ 𝜒)) → (𝜒 → (𝜓 → 𝜑)))

(Contributed by Alan Sare, 22-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ ((𝜑 ↔ (𝜓 ∧ 𝜒)) → (𝜒 → (𝜓 → 𝜑)))

Theorem

onfrALTlem2VD 45005*

Virtual deduction proof of onfrALTlem2 44663. 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. onfrALTlem2 44663 is onfrALTlem2VD 45005 without virtual deductions and was automatically derived from onfrALTlem2VD 45005.

1::	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅), ((𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅) ∧ 𝑧 ∈ (𝑎 ∩ 𝑦))   ▶   ((𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅) ∧ 𝑧 ∈ (𝑎 ∩ 𝑦))   )
2:1:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅), ((𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅) ∧ 𝑧 ∈ (𝑎 ∩ 𝑦))   ▶   𝑧 ∈ (𝑎 ∩ 𝑦)   )
3:2:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅), ((𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅) ∧ 𝑧 ∈ (𝑎 ∩ 𝑦))   ▶   𝑧 ∈ 𝑎   )
4::	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ▶   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   )
5::	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   )
6:5:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   𝑥 ∈ 𝑎   )
7:4:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ▶   𝑎 ⊆ On   )
8:6,7:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   𝑥 ∈ On   )
9:8:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   Ord 𝑥   )
10:9:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   Tr 𝑥   )
11:1:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅), ((𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅) ∧ 𝑧 ∈ (𝑎 ∩ 𝑦))   ▶   𝑦 ∈ (𝑎 ∩ 𝑥)   )
12:11:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅), ((𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅) ∧ 𝑧 ∈ (𝑎 ∩ 𝑦))   ▶   𝑦 ∈ 𝑥   )
13:2:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅), ((𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅) ∧ 𝑧 ∈ (𝑎 ∩ 𝑦))   ▶   𝑧 ∈ 𝑦   )
14:10,12,13:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅), ((𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅) ∧ 𝑧 ∈ (𝑎 ∩ 𝑦))   ▶   𝑧 ∈ 𝑥   )
15:3,14:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅), ((𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅) ∧ 𝑧 ∈ (𝑎 ∩ 𝑦))   ▶   𝑧 ∈ (𝑎 ∩ 𝑥)   )
16:13,15:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅), ((𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅) ∧ 𝑧 ∈ (𝑎 ∩ 𝑦))   ▶   𝑧 ∈ ((𝑎 ∩ 𝑥) ∩ 𝑦)   )
17:16:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅), (𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦 ) = ∅)   ▶   (𝑧 ∈ (𝑎 ∩ 𝑦) → 𝑧 ∈ ((𝑎 ∩ 𝑥) ∩ 𝑦))   )
18:17:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅), (𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦 ) = ∅)   ▶   ∀𝑧(𝑧 ∈ (𝑎 ∩ 𝑦) → 𝑧 ∈ ((𝑎 ∩ 𝑥) ∩ 𝑦))   )
19:18:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅), (𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦 ) = ∅)   ▶   (𝑎 ∩ 𝑦) ⊆ ((𝑎 ∩ 𝑥) ∩ 𝑦)   )
20::	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅), (𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦 ) = ∅)   ▶   (𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅)   )
21:20:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅), (𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦 ) = ∅)   ▶   ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅   )
22:19,21:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅), (𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦 ) = ∅)   ▶   (𝑎 ∩ 𝑦) = ∅   )
23:20:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅), (𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦 ) = ∅)   ▶   𝑦 ∈ (𝑎 ∩ 𝑥)   )
24:23:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅), (𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦 ) = ∅)   ▶   𝑦 ∈ 𝑎   )
25:22,24:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅), (𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦 ) = ∅)   ▶   (𝑦 ∈ 𝑎 ∧ (𝑎 ∩ 𝑦) = ∅)   )
26:25:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   ((𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅) → (𝑦 ∈ 𝑎 ∧ (𝑎 ∩ 𝑦) = ∅))   )
27:26:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   ∀𝑦((𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥 ) ∩ 𝑦) = ∅) → (𝑦 ∈ 𝑎 ∧ (𝑎 ∩ 𝑦) = ∅))   )
28:27:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   (∃𝑦(𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥 ) ∩ 𝑦) = ∅) → ∃𝑦(𝑦 ∈ 𝑎 ∧ (𝑎 ∩ 𝑦) = ∅))   )
29::	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   ∃𝑦 ∈ (𝑎 ∩ 𝑥)((𝑎 ∩ 𝑥) ∩ 𝑦 ) = ∅   )
30:29:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   ∃𝑦(𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅)   )
31:28,30:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   ∃𝑦(𝑦 ∈ 𝑎 ∧ (𝑎 ∩ 𝑦) = ∅)   )
qed:31:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   ∃𝑦 ∈ 𝑎(𝑎 ∩ 𝑦) = ∅   )

(Contributed by Alan Sare, 22-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   ∃𝑦 ∈ 𝑎 (𝑎 ∩ 𝑦) = ∅   )

Theorem

onfrALTlem1VD 45006*

Virtual deduction proof of onfrALTlem1 44665. 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. onfrALTlem1 44665 is onfrALTlem1VD 45006 without virtual deductions and was automatically derived from onfrALTlem1VD 45006.

1::	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ (𝑎 ∩ 𝑥) = ∅)   ▶   (𝑥 ∈ 𝑎 ∧ (𝑎 ∩ 𝑥) = ∅)   )
2:1:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ (𝑎 ∩ 𝑥) = ∅)   ▶   ∃𝑥(𝑥 ∈ 𝑎 ∧ (𝑎 ∩ 𝑥) = ∅)   )
3:2:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ (𝑎 ∩ 𝑥) = ∅)   ▶   ∃𝑦[𝑦 / 𝑥](𝑥 ∈ 𝑎 ∧ (𝑎 ∩ 𝑥) = ∅)    )
4::	⊢ ([𝑦 / 𝑥](𝑥 ∈ 𝑎 ∧ (𝑎 ∩ 𝑥) = ∅ ) ↔ (𝑦 ∈ 𝑎 ∧ (𝑎 ∩ 𝑦) = ∅))
5:4:	⊢ ∀𝑦([𝑦 / 𝑥](𝑥 ∈ 𝑎 ∧ (𝑎 ∩ 𝑥) = ∅) ↔ (𝑦 ∈ 𝑎 ∧ (𝑎 ∩ 𝑦) = ∅))
6:5:	⊢ (∃𝑦[𝑦 / 𝑥](𝑥 ∈ 𝑎 ∧ (𝑎 ∩ 𝑥) = ∅) ↔ ∃𝑦(𝑦 ∈ 𝑎 ∧ (𝑎 ∩ 𝑦) = ∅))
7:3,6:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ (𝑎 ∩ 𝑥) = ∅)   ▶   ∃𝑦(𝑦 ∈ 𝑎 ∧ (𝑎 ∩ 𝑦) = ∅)   )
8::	⊢ (∃𝑦 ∈ 𝑎(𝑎 ∩ 𝑦) = ∅ ↔ ∃𝑦( 𝑦 ∈ 𝑎 ∧ (𝑎 ∩ 𝑦) = ∅))
qed:7,8:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ (𝑎 ∩ 𝑥) = ∅)   ▶   ∃𝑦 ∈ 𝑎(𝑎 ∩ 𝑦) = ∅   )

(Contributed by Alan Sare, 22-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ (𝑎 ∩ 𝑥) = ∅)   ▶   ∃𝑦 ∈ 𝑎 (𝑎 ∩ 𝑦) = ∅   )

Theorem

onfrALTVD 45007

Virtual deduction proof of onfrALT 44666. 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. onfrALT 44666 is onfrALTVD 45007 without virtual deductions and was automatically derived from onfrALTVD 45007.

1::	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   ∃𝑦 ∈ 𝑎(𝑎 ∩ 𝑦) = ∅   )
2::	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ (𝑎 ∩ 𝑥) = ∅)   ▶   ∃𝑦 ∈ 𝑎(𝑎 ∩ 𝑦) = ∅   )
3:1:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   𝑥 ∈ 𝑎   ▶    (¬ (𝑎 ∩ 𝑥) = ∅ → ∃𝑦 ∈ 𝑎(𝑎 ∩ 𝑦) = ∅)   )
4:2:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   𝑥 ∈ 𝑎   ▶    ((𝑎 ∩ 𝑥) = ∅ → ∃𝑦 ∈ 𝑎(𝑎 ∩ 𝑦) = ∅)   )
5::	⊢ ((𝑎 ∩ 𝑥) = ∅ ∨ ¬ (𝑎 ∩ 𝑥) = ∅)
6:5,4,3:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   𝑥 ∈ 𝑎   ▶    ∃𝑦 ∈ 𝑎(𝑎 ∩ 𝑦) = ∅   )
7:6:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ▶   (𝑥 ∈ 𝑎 → ∃𝑦 ∈ 𝑎(𝑎 ∩ 𝑦) = ∅)   )
8:7:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ▶   ∀𝑥(𝑥 ∈ 𝑎 → ∃𝑦 ∈ 𝑎(𝑎 ∩ 𝑦) = ∅)   )
9:8:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ▶   (∃𝑥𝑥 ∈ 𝑎 → ∃𝑦 ∈ 𝑎(𝑎 ∩ 𝑦) = ∅)   )
10::	⊢ (𝑎 ≠ ∅ ↔ ∃𝑥𝑥 ∈ 𝑎)
11:9,10:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ▶   (𝑎 ≠ ∅ → ∃𝑦 ∈ 𝑎(𝑎 ∩ 𝑦) = ∅)   )
12::	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ▶   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   )
13:12:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ▶   𝑎 ≠ ∅   )
14:13,11:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ▶   ∃𝑦 ∈ 𝑎(𝑎 ∩ 𝑦) = ∅   )
15:14:	⊢ ((𝑎 ⊆ On ∧ 𝑎 ≠ ∅) → ∃𝑦 ∈ 𝑎 (𝑎 ∩ 𝑦) = ∅)
16:15:	⊢ ∀𝑎((𝑎 ⊆ On ∧ 𝑎 ≠ ∅) → ∃𝑦 ∈ 𝑎(𝑎 ∩ 𝑦) = ∅)
qed:16:	⊢ E Fr On

(Contributed by Alan Sare, 22-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ E Fr On

Theorem

csbeq2gVD 45008

Virtual deduction proof of csbeq2 3851. 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. csbeq2 3851 is csbeq2gVD 45008 without virtual deductions and was automatically derived from csbeq2gVD 45008.

1::	⊢ (   𝐴 ∈ 𝑉   ▶   𝐴 ∈ 𝑉   )
2:1:	⊢ (   𝐴 ∈ 𝑉   ▶   (∀𝑥𝐵 = 𝐶 → [𝐴 / 𝑥] 𝐵 = 𝐶)   )
3:1:	⊢ (   𝐴 ∈ 𝑉   ▶   ([𝐴 / 𝑥]𝐵 = 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶)   )
4:2,3:	⊢ (   𝐴 ∈ 𝑉   ▶   (∀𝑥𝐵 = 𝐶 → ⦋𝐴 / 𝑥 ⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶)   )
qed:4:	⊢ (𝐴 ∈ 𝑉 → (∀𝑥𝐵 = 𝐶 → ⦋𝐴 / 𝑥⦌ 𝐵 = ⦋𝐴 / 𝑥⦌𝐶))

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

⊢ (𝐴 ∈ 𝑉 → (∀𝑥 𝐵 = 𝐶 → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶))

Theorem

csbsngVD 45009

Virtual deduction proof of csbsng 4660. 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. csbsng 4660 is csbsngVD 45009 without virtual deductions and was automatically derived from csbsngVD 45009.

1::	⊢ (   𝐴 ∈ 𝑉   ▶   𝐴 ∈ 𝑉   )
2:1:	⊢ (   𝐴 ∈ 𝑉   ▶   ([𝐴 / 𝑥]𝑦 = 𝐵 ↔ ⦋𝐴 / 𝑥⦌𝑦 = ⦋𝐴 / 𝑥⦌𝐵)   )
3:1:	⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌𝑦 = 𝑦   )
4:3:	⊢ (   𝐴 ∈ 𝑉   ▶   (⦋𝐴 / 𝑥⦌𝑦 = ⦋𝐴 / 𝑥⦌𝐵 ↔ 𝑦 = ⦋𝐴 / 𝑥⦌𝐵)   )
5:2,4:	⊢ (   𝐴 ∈ 𝑉   ▶   ([𝐴 / 𝑥]𝑦 = 𝐵 ↔ 𝑦 = ⦋𝐴 / 𝑥⦌𝐵)   )
6:5:	⊢ (   𝐴 ∈ 𝑉   ▶   ∀𝑦([𝐴 / 𝑥]𝑦 = 𝐵 ↔ 𝑦 = ⦋𝐴 / 𝑥⦌𝐵)   )
7:6:	⊢ (   𝐴 ∈ 𝑉   ▶   {𝑦 ∣ [𝐴 / 𝑥]𝑦 = 𝐵} = {𝑦 ∣ 𝑦 = ⦋𝐴 / 𝑥⦌𝐵}   )
8:1:	⊢ (   𝐴 ∈ 𝑉   ▶   {𝑦 ∣ [𝐴 / 𝑥]𝑦 = 𝐵} = ⦋𝐴 / 𝑥⦌{𝑦 ∣ 𝑦 = 𝐵}   )
9:7,8:	⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌{𝑦 ∣ 𝑦 = 𝐵} = {𝑦 ∣ 𝑦 = ⦋𝐴 / 𝑥⦌𝐵}   )
10::	⊢ {𝐵} = {𝑦 ∣ 𝑦 = 𝐵}
11:10:	⊢ ∀𝑥{𝐵} = {𝑦 ∣ 𝑦 = 𝐵}
12:1,11:	⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌{𝐵} = ⦋ 𝐴 / 𝑥⦌{𝑦 ∣ 𝑦 = 𝐵}   )
13:9,12:	⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌{𝐵} = { 𝑦 ∣ 𝑦 = ⦋𝐴 / 𝑥⦌𝐵}   )
14::	⊢ {⦋𝐴 / 𝑥⦌𝐵} = {𝑦 ∣ 𝑦 = ⦋𝐴 / 𝑥⦌𝐵}
15:13,14:	⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌{𝐵} = { ⦋𝐴 / 𝑥⦌𝐵}   )
qed:15:	⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌{𝐵} = {⦋ 𝐴 / 𝑥⦌𝐵})

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

⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌{𝐵} = {⦋𝐴 / 𝑥⦌𝐵})

Theorem

csbxpgVD 45010

Virtual deduction proof of csbxp 5720. 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. csbxp 5720 is csbxpgVD 45010 without virtual deductions and was automatically derived from csbxpgVD 45010.

1::	⊢ (   𝐴 ∈ 𝑉   ▶   𝐴 ∈ 𝑉   )
2:1:	⊢ (   𝐴 ∈ 𝑉   ▶   ([𝐴 / 𝑥]𝑤 ∈ 𝐵 ↔ ⦋𝐴 / 𝑥⦌𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵)   )
3:1:	⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌𝑤 = 𝑤   )
4:3:	⊢ (   𝐴 ∈ 𝑉   ▶   (⦋𝐴 / 𝑥⦌𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵 ↔ 𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵)   )
5:2,4:	⊢ (   𝐴 ∈ 𝑉   ▶   ([𝐴 / 𝑥]𝑤 ∈ 𝐵 ↔ 𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵)   )
6:1:	⊢ (   𝐴 ∈ 𝑉   ▶   ([𝐴 / 𝑥]𝑦 ∈ 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶)   )
7:1:	⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌𝑦 = 𝑦   )
8:7:	⊢ (   𝐴 ∈ 𝑉   ▶   (⦋𝐴 / 𝑥⦌𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 ↔ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶)   )
9:6,8:	⊢ (   𝐴 ∈ 𝑉   ▶   ([𝐴 / 𝑥]𝑦 ∈ 𝐶 ↔ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶)   )
10:5,9:	⊢ (   𝐴 ∈ 𝑉   ▶   (([𝐴 / 𝑥]𝑤 ∈ 𝐵 ∧ [𝐴 / 𝑥]𝑦 ∈ 𝐶) ↔ (𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶))   )
11:1:	⊢ (   𝐴 ∈ 𝑉   ▶   ([𝐴 / 𝑥](𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶) ↔ ([𝐴 / 𝑥]𝑤 ∈ 𝐵 ∧ [𝐴 / 𝑥]𝑦 ∈ 𝐶))   )
12:10,11:	⊢ (   𝐴 ∈ 𝑉   ▶   ([𝐴 / 𝑥](𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶) ↔ (𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶))   )
13:1:	⊢ (   𝐴 ∈ 𝑉   ▶   ([𝐴 / 𝑥]𝑧 = ⟨𝑤   ,    𝑦⟩ ↔ 𝑧 = ⟨𝑤, 𝑦⟩)   )
14:12,13:	⊢ (   𝐴 ∈ 𝑉   ▶   (([𝐴 / 𝑥]𝑧 = ⟨𝑤    ,   𝑦⟩ ∧ [𝐴 / 𝑥](𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ (𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶)))   )
15:1:	⊢ (   𝐴 ∈ 𝑉   ▶   ([𝐴 / 𝑥](𝑧 = ⟨𝑤    ,   𝑦⟩ ∧ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ ([𝐴 / 𝑥]𝑧 = ⟨𝑤, 𝑦⟩ ∧ [𝐴 / 𝑥](𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)))   )
16:14,15:	⊢ (   𝐴 ∈ 𝑉   ▶   ([𝐴 / 𝑥](𝑧 = ⟨𝑤    ,   𝑦⟩ ∧ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ (𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶)))   )
17:16:	⊢ (   𝐴 ∈ 𝑉   ▶   ∀𝑦([𝐴 / 𝑥](𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ (𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶)))   )
18:17:	⊢ (   𝐴 ∈ 𝑉   ▶   (∃𝑦[𝐴 / 𝑥](𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ ∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶)))   )
19:1:	⊢ (   𝐴 ∈ 𝑉   ▶   ([𝐴 / 𝑥]∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ ∃𝑦[𝐴 / 𝑥](𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)))   )
20:18,19:	⊢ (   𝐴 ∈ 𝑉   ▶   ([𝐴 / 𝑥]∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ ∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶)))   )
21:20:	⊢ (   𝐴 ∈ 𝑉   ▶   ∀𝑤([𝐴 / 𝑥]∃𝑦( 𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ ∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶)))   )
22:21:	⊢ (   𝐴 ∈ 𝑉   ▶   (∃𝑤[𝐴 / 𝑥]∃𝑦( 𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ ∃𝑤∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶)))   )
23:1:	⊢ (   𝐴 ∈ 𝑉   ▶   ([𝐴 / 𝑥]∃𝑤∃𝑦( 𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ ∃𝑤[𝐴 / 𝑥]∃𝑦 (𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)))   )
24:22,23:	⊢ (   𝐴 ∈ 𝑉   ▶   ([𝐴 / 𝑥]∃𝑤∃𝑦( 𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ ∃𝑤∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶)))   )
25:24:	⊢ (   𝐴 ∈ 𝑉   ▶   ∀𝑧([𝐴 / 𝑥]∃𝑤∃ 𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ ∃𝑤∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶)))   )
26:25:	⊢ (   𝐴 ∈ 𝑉   ▶   {𝑧 ∣ [𝐴 / 𝑥]∃𝑤∃ 𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))} = {𝑧 ∣ ∃𝑤∃𝑦( 𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶))}    )
27:1:	⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌{𝑧 ∣ ∃𝑤∃ 𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))} = {𝑧 ∣ [𝐴 / 𝑥] ∃𝑤∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))}   )
28:26,27:	⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌{𝑧 ∣ ∃𝑤∃ 𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))} = {𝑧 ∣ ∃𝑤∃𝑦( 𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶))}    )
29::	⊢ {⟨𝑤   ,   𝑦⟩ ∣ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)} = {𝑧 ∣ ∃𝑤∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))}
30::	⊢ (𝐵 × 𝐶) = {⟨𝑤   ,   𝑦⟩ ∣ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)}
31:29,30:	⊢ (𝐵 × 𝐶) = {𝑧 ∣ ∃𝑤∃𝑦(𝑧 = ⟨𝑤 , 𝑦⟩ ∧ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))}
32:31:	⊢ ∀𝑥(𝐵 × 𝐶) = {𝑧 ∣ ∃𝑤∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))}
33:1,32:	⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌(𝐵 × 𝐶) = ⦋𝐴 / 𝑥⦌{𝑧 ∣ ∃𝑤∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))}   )
34:28,33:	⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌(𝐵 × 𝐶) = {𝑧 ∣ ∃𝑤∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶))}   )
35::	⊢ {⟨𝑤   ,   𝑦⟩ ∣ (𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶)} = {𝑧 ∣ ∃𝑤∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶))}
36::	⊢ (⦋𝐴 / 𝑥⦌𝐵 × ⦋𝐴 / 𝑥⦌𝐶) = { ⟨𝑤, 𝑦⟩ ∣ (𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶)}
37:35,36:	⊢ (⦋𝐴 / 𝑥⦌𝐵 × ⦋𝐴 / 𝑥⦌𝐶) = {𝑧 ∣ ∃𝑤∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶))}
38:34,37:	⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌(𝐵 × 𝐶) = (⦋𝐴 / 𝑥⦌𝐵 × ⦋𝐴 / 𝑥⦌𝐶)   )
qed:38:	⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(𝐵 × 𝐶) = ( ⦋𝐴 / 𝑥⦌𝐵 × ⦋𝐴 / 𝑥⦌𝐶))

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

⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(𝐵 × 𝐶) = (⦋𝐴 / 𝑥⦌𝐵 × ⦋𝐴 / 𝑥⦌𝐶))

Theorem

csbresgVD 45011

Virtual deduction proof of csbres 5935. 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. csbres 5935 is csbresgVD 45011 without virtual deductions and was automatically derived from csbresgVD 45011.

1::	⊢ (   𝐴 ∈ 𝑉   ▶   𝐴 ∈ 𝑉   )
2:1:	⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌V = V   )
3:2:	⊢ (   𝐴 ∈ 𝑉   ▶   (⦋𝐴 / 𝑥⦌𝐶 × ⦋𝐴 / 𝑥⦌V) = (⦋𝐴 / 𝑥⦌𝐶 × V)   )
4:1:	⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌(𝐶 × V) = (⦋𝐴 / 𝑥⦌𝐶 × ⦋𝐴 / 𝑥⦌V)   )
5:3,4:	⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌(𝐶 × V) = (⦋𝐴 / 𝑥⦌𝐶 × V)   )
6:5:	⊢ (   𝐴 ∈ 𝑉   ▶   (⦋𝐴 / 𝑥⦌𝐵 ∩ ⦋𝐴 / 𝑥⦌(𝐶 × V)) = (⦋𝐴 / 𝑥⦌𝐵 ∩ (⦋𝐴 / 𝑥⦌𝐶 × V))   )
7:1:	⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌(𝐵 ∩ (𝐶 × V)) = (⦋𝐴 / 𝑥⦌𝐵 ∩ ⦋𝐴 / 𝑥⦌(𝐶 × V))   )
8:6,7:	⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌(𝐵 ∩ (𝐶 × V)) = (⦋𝐴 / 𝑥⦌𝐵 ∩ (⦋𝐴 / 𝑥⦌𝐶 × V))   )
9::	⊢ (𝐵 ↾ 𝐶) = (𝐵 ∩ (𝐶 × V))
10:9:	⊢ ∀𝑥(𝐵 ↾ 𝐶) = (𝐵 ∩ (𝐶 × V))
11:1,10:	⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌(𝐵 ↾ 𝐶) = ⦋𝐴 / 𝑥⦌(𝐵 ∩ (𝐶 × V))   )
12:8,11:	⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌(𝐵 ↾ 𝐶) = ( ⦋𝐴 / 𝑥⦌𝐵 ∩ (⦋𝐴 / 𝑥⦌𝐶 × V))   )
13::	⊢ (⦋𝐴 / 𝑥⦌𝐵 ↾ ⦋𝐴 / 𝑥⦌𝐶) = ( ⦋𝐴 / 𝑥⦌𝐵 ∩ (⦋𝐴 / 𝑥⦌𝐶 × V))
14:12,13:	⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌(𝐵 ↾ 𝐶) = ( ⦋𝐴 / 𝑥⦌𝐵 ↾ ⦋𝐴 / 𝑥⦌𝐶)   )
qed:14:	⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(𝐵 ↾ 𝐶) = ( ⦋𝐴 / 𝑥⦌𝐵 ↾ ⦋𝐴 / 𝑥⦌𝐶))

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

⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(𝐵 ↾ 𝐶) = (⦋𝐴 / 𝑥⦌𝐵 ↾ ⦋𝐴 / 𝑥⦌𝐶))

Theorem

csbrngVD 45012

Virtual deduction proof of csbrn 6155. 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. csbrn 6155 is csbrngVD 45012 without virtual deductions and was automatically derived from csbrngVD 45012.

1::	⊢ (   𝐴 ∈ 𝑉   ▶   𝐴 ∈ 𝑉   )
2:1:	⊢ (   𝐴 ∈ 𝑉   ▶   ([𝐴 / 𝑥]⟨𝑤   ,   𝑦⟩ ∈ 𝐵 ↔ ⦋𝐴 / 𝑥⦌⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵)   )
3:1:	⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌⟨𝑤   ,   𝑦⟩ = ⟨𝑤, 𝑦⟩   )
4:3:	⊢ (   𝐴 ∈ 𝑉   ▶   (⦋𝐴 / 𝑥⦌⟨𝑤   ,   𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵 ↔ ⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵)   )
5:2,4:	⊢ (   𝐴 ∈ 𝑉   ▶   ([𝐴 / 𝑥]⟨𝑤   ,   𝑦⟩ ∈ 𝐵 ↔ ⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵)   )
6:5:	⊢ (   𝐴 ∈ 𝑉   ▶   ∀𝑤([𝐴 / 𝑥]⟨𝑤   ,    𝑦⟩ ∈ 𝐵 ↔ ⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵)   )
7:6:	⊢ (   𝐴 ∈ 𝑉   ▶   (∃𝑤[𝐴 / 𝑥]⟨𝑤   ,    𝑦⟩ ∈ 𝐵 ↔ ∃𝑤⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵)   )
8:1:	⊢ (   𝐴 ∈ 𝑉   ▶   (∃𝑤[𝐴 / 𝑥]⟨𝑤   ,    𝑦⟩ ∈ 𝐵 ↔ [𝐴 / 𝑥]∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵)   )
9:7,8:	⊢ (   𝐴 ∈ 𝑉   ▶   ([𝐴 / 𝑥]∃𝑤⟨𝑤    ,   𝑦⟩ ∈ 𝐵 ↔ ∃𝑤⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵)   )
10:9:	⊢ (   𝐴 ∈ 𝑉   ▶   ∀𝑦([𝐴 / 𝑥]∃𝑤 ⟨𝑤, 𝑦⟩ ∈ 𝐵 ↔ ∃𝑤⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵)   )
11:10:	⊢ (   𝐴 ∈ 𝑉   ▶   {𝑦 ∣ [𝐴 / 𝑥]∃𝑤⟨ 𝑤, 𝑦⟩ ∈ 𝐵} = {𝑦 ∣ ∃𝑤⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵}   )
12:1:	⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌{𝑦 ∣ ∃𝑤 ⟨𝑤, 𝑦⟩ ∈ 𝐵} = {𝑦 ∣ [𝐴 / 𝑥]∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵}   )
13:11,12:	⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌{𝑦 ∣ ∃𝑤 ⟨𝑤, 𝑦⟩ ∈ 𝐵} = {𝑦 ∣ ∃𝑤⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵}   )
14::	⊢ ran 𝐵 = {𝑦 ∣ ∃𝑤⟨𝑤   ,   𝑦⟩ ∈ 𝐵}
15:14:	⊢ ∀𝑥ran 𝐵 = {𝑦 ∣ ∃𝑤⟨𝑤   ,   𝑦⟩ ∈ 𝐵}
16:1,15:	⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌ran 𝐵 = ⦋𝐴 / 𝑥⦌{𝑦 ∣ ∃𝑤⟨𝑤, 𝑦⟩ ∈ 𝐵}   )
17:13,16:	⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌ran 𝐵 = {𝑦 ∣ ∃𝑤⟨𝑤, 𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵}   )
18::	⊢ ran ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ ∃𝑤⟨𝑤    ,   𝑦⟩ ∈ ⦋𝐴 / 𝑥⦌𝐵}
19:17,18:	⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌ran 𝐵 = ran ⦋ 𝐴 / 𝑥⦌𝐵   )
qed:19:	⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌ran 𝐵 = ran ⦋𝐴 / 𝑥⦌𝐵)

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

⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌ran 𝐵 = ran ⦋𝐴 / 𝑥⦌𝐵)

Theorem

csbima12gALTVD 45013

Virtual deduction proof of csbima12 6032. 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. csbima12 6032 is csbima12gALTVD 45013 without virtual deductions and was automatically derived from csbima12gALTVD 45013.

1::	⊢ (   𝐴 ∈ 𝐶   ▶   𝐴 ∈ 𝐶   )
2:1:	⊢ (   𝐴 ∈ 𝐶   ▶   ⦋𝐴 / 𝑥⦌(𝐹 ↾ 𝐵) = ( ⦋𝐴 / 𝑥⦌𝐹 ↾ ⦋𝐴 / 𝑥⦌𝐵)   )
3:2:	⊢ (   𝐴 ∈ 𝐶   ▶    ran ⦋𝐴 / 𝑥⦌(𝐹 ↾ 𝐵) = ran (⦋𝐴 / 𝑥⦌𝐹 ↾ ⦋𝐴 / 𝑥⦌𝐵)   )
4:1:	⊢ (   𝐴 ∈ 𝐶   ▶    ⦋𝐴 / 𝑥⦌ran (𝐹 ↾ 𝐵) = ran ⦋𝐴 / 𝑥⦌(𝐹 ↾ 𝐵)   )
5:3,4:	⊢ (   𝐴 ∈ 𝐶   ▶    ⦋𝐴 / 𝑥⦌ran (𝐹 ↾ 𝐵) = ran (⦋𝐴 / 𝑥⦌𝐹 ↾ ⦋𝐴 / 𝑥⦌𝐵)   )
6::	⊢ (𝐹 “ 𝐵) = ran (𝐹 ↾ 𝐵)
7:6:	⊢ ∀𝑥(𝐹 “ 𝐵) = ran (𝐹 ↾ 𝐵)
8:1,7:	⊢ (   𝐴 ∈ 𝐶   ▶   ⦋𝐴 / 𝑥⦌(𝐹 “ 𝐵) = ⦋ 𝐴 / 𝑥⦌ran (𝐹 ↾ 𝐵)   )
9:5,8:	⊢ (   𝐴 ∈ 𝐶   ▶   ⦋𝐴 / 𝑥⦌(𝐹 “ 𝐵) = ran (⦋𝐴 / 𝑥⦌𝐹 ↾ ⦋𝐴 / 𝑥⦌𝐵)   )
10::	⊢ (⦋𝐴 / 𝑥⦌𝐹 “ ⦋𝐴 / 𝑥⦌𝐵) = ran (⦋𝐴 / 𝑥⦌𝐹 ↾ ⦋𝐴 / 𝑥⦌𝐵)
11:9,10:	⊢ (   𝐴 ∈ 𝐶   ▶   ⦋𝐴 / 𝑥⦌(𝐹 “ 𝐵) = ( ⦋𝐴 / 𝑥⦌𝐹 “ ⦋𝐴 / 𝑥⦌𝐵)   )
qed:11:	⊢ (𝐴 ∈ 𝐶 → ⦋𝐴 / 𝑥⦌(𝐹 “ 𝐵) = (⦋ 𝐴 / 𝑥⦌𝐹 “ ⦋𝐴 / 𝑥⦌𝐵))

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

⊢ (𝐴 ∈ 𝐶 → ⦋𝐴 / 𝑥⦌(𝐹 “ 𝐵) = (⦋𝐴 / 𝑥⦌𝐹 “ ⦋𝐴 / 𝑥⦌𝐵))

Theorem

csbunigVD 45014

Virtual deduction proof of csbuni 4888. 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. csbuni 4888 is csbunigVD 45014 without virtual deductions and was automatically derived from csbunigVD 45014.

1::	⊢ (   𝐴 ∈ 𝑉   ▶   𝐴 ∈ 𝑉   )
2:1:	⊢ (   𝐴 ∈ 𝑉   ▶   ([𝐴 / 𝑥]𝑧 ∈ 𝑦 ↔ 𝑧 ∈ 𝑦)   )
3:1:	⊢ (   𝐴 ∈ 𝑉   ▶   ([𝐴 / 𝑥]𝑦 ∈ 𝐵 ↔ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐵)   )
4:2,3:	⊢ (   𝐴 ∈ 𝑉   ▶   (([𝐴 / 𝑥]𝑧 ∈ 𝑦 ∧ [𝐴 / 𝑥]𝑦 ∈ 𝐵) ↔ (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐵))   )
5:1:	⊢ (   𝐴 ∈ 𝑉   ▶   ([𝐴 / 𝑥](𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵) ↔ ([𝐴 / 𝑥]𝑧 ∈ 𝑦 ∧ [𝐴 / 𝑥]𝑦 ∈ 𝐵))   )
6:4,5:	⊢ (   𝐴 ∈ 𝑉   ▶   ([𝐴 / 𝑥](𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵) ↔ (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐵))   )
7:6:	⊢ (   𝐴 ∈ 𝑉   ▶   ∀𝑦([𝐴 / 𝑥](𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵) ↔ (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐵))   )
8:7:	⊢ (   𝐴 ∈ 𝑉   ▶   (∃𝑦[𝐴 / 𝑥](𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵) ↔ ∃𝑦(𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐵))   )
9:1:	⊢ (   𝐴 ∈ 𝑉   ▶   ([𝐴 / 𝑥]∃𝑦(𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵) ↔ ∃𝑦[𝐴 / 𝑥](𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵))   )
10:8,9:	⊢ (   𝐴 ∈ 𝑉   ▶   ([𝐴 / 𝑥]∃𝑦(𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵) ↔ ∃𝑦(𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐵))   )
11:10:	⊢ (   𝐴 ∈ 𝑉   ▶   ∀𝑧([𝐴 / 𝑥]∃𝑦( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵) ↔ ∃𝑦(𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐵))   )
12:11:	⊢ (   𝐴 ∈ 𝑉   ▶   {𝑧 ∣ [𝐴 / 𝑥]∃𝑦( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)} = {𝑧 ∣ ∃𝑦(𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐵)}   )
13:1:	⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌{𝑧 ∣ ∃𝑦(𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)} = {𝑧 ∣ [𝐴 / 𝑥]∃𝑦(𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)}    )
14:12,13:	⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌{𝑧 ∣ ∃𝑦(𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)} = {𝑧 ∣ ∃𝑦(𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐵)}   )
15::	⊢ ∪ 𝐵 = {𝑧 ∣ ∃𝑦(𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)}
16:15:	⊢ ∀𝑥∪ 𝐵 = {𝑧 ∣ ∃𝑦(𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)}
17:1,16:	⊢ (   𝐴 ∈ 𝑉   ▶   [𝐴 / 𝑥]∪ 𝐵 = {𝑧 ∣ ∃𝑦(𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)}   )
18:1,17:	⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌∪ 𝐵 = ⦋𝐴 / 𝑥⦌{𝑧 ∣ ∃𝑦(𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)}   )
19:14,18:	⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌∪ 𝐵 = {𝑧 ∣ ∃𝑦(𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐵)}   )
20::	⊢ ∪ ⦋𝐴 / 𝑥⦌𝐵 = {𝑧 ∣ ∃𝑦(𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐵)}
21:19,20:	⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌∪ 𝐵 = ∪ ⦋𝐴 / 𝑥⦌𝐵   )
qed:21:	⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌∪ 𝐵 = ∪ ⦋𝐴 / 𝑥⦌𝐵)

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

⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌∪ 𝐵 = ∪ ⦋𝐴 / 𝑥⦌𝐵)

Theorem

csbfv12gALTVD 45015

Virtual deduction proof of csbfv12 6873. 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. csbfv12 6873 is csbfv12gALTVD 45015 without virtual deductions and was automatically derived from csbfv12gALTVD 45015.

1::	⊢ (   𝐴 ∈ 𝐶   ▶   𝐴 ∈ 𝐶   )
2:1:	⊢ (   𝐴 ∈ 𝐶   ▶   ⦋𝐴 / 𝑥⦌{𝑦} = { 𝑦}   )
3:1:	⊢ (   𝐴 ∈ 𝐶   ▶   ⦋𝐴 / 𝑥⦌(𝐹 “ {𝐵 }) = (⦋𝐴 / 𝑥⦌𝐹 “ ⦋𝐴 / 𝑥⦌{𝐵})   )
4:1:	⊢ (   𝐴 ∈ 𝐶   ▶   ⦋𝐴 / 𝑥⦌{𝐵} = { ⦋𝐴 / 𝑥⦌𝐵}   )
5:4:	⊢ (   𝐴 ∈ 𝐶   ▶   (⦋𝐴 / 𝑥⦌𝐹 “ ⦋𝐴 / 𝑥⦌{𝐵}) = (⦋𝐴 / 𝑥⦌𝐹 “ {⦋𝐴 / 𝑥⦌𝐵})   )
6:3,5:	⊢ (   𝐴 ∈ 𝐶   ▶   ⦋𝐴 / 𝑥⦌(𝐹 “ {𝐵 }) = (⦋𝐴 / 𝑥⦌𝐹 “ {⦋𝐴 / 𝑥⦌𝐵})   )
7:1:	⊢ (   𝐴 ∈ 𝐶   ▶   ([𝐴 / 𝑥](𝐹 “ { 𝐵}) = {𝑦} ↔ ⦋𝐴 / 𝑥⦌(𝐹 “ {𝐵}) = ⦋𝐴 / 𝑥⦌{𝑦})   )
8:6,2:	⊢ (   𝐴 ∈ 𝐶   ▶   (⦋𝐴 / 𝑥⦌(𝐹 “ { 𝐵}) = ⦋𝐴 / 𝑥⦌{𝑦} ↔ (⦋𝐴 / 𝑥⦌𝐹 “ {⦋𝐴 / 𝑥⦌𝐵}) = {𝑦})   )
9:7,8:	⊢ (   𝐴 ∈ 𝐶   ▶   ([𝐴 / 𝑥](𝐹 “ { 𝐵}) = {𝑦} ↔ (⦋𝐴 / 𝑥⦌𝐹 “ {⦋𝐴 / 𝑥⦌𝐵}) = {𝑦})    )
10:9:	⊢ (   𝐴 ∈ 𝐶   ▶   ∀𝑦([𝐴 / 𝑥](𝐹 “ {𝐵}) = {𝑦} ↔ (⦋𝐴 / 𝑥⦌𝐹 “ {⦋𝐴 / 𝑥⦌𝐵}) = {𝑦})   )
11:10:	⊢ (   𝐴 ∈ 𝐶   ▶   {𝑦 ∣ [𝐴 / 𝑥](𝐹 “ {𝐵}) = {𝑦}} = {𝑦 ∣ (⦋𝐴 / 𝑥⦌𝐹 “ {⦋𝐴 / 𝑥⦌𝐵}) = {𝑦}}   )
12:1:	⊢ (   𝐴 ∈ 𝐶   ▶   ⦋𝐴 / 𝑥⦌{𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} = {𝑦 ∣ [𝐴 / 𝑥](𝐹 “ {𝐵}) = {𝑦}}   )
13:11,12:	⊢ (   𝐴 ∈ 𝐶   ▶   ⦋𝐴 / 𝑥⦌{𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} = {𝑦 ∣ (⦋𝐴 / 𝑥⦌𝐹 “ {⦋𝐴 / 𝑥⦌𝐵}) = {𝑦 }}   )
14:13:	⊢ (   𝐴 ∈ 𝐶   ▶   ∪ ⦋𝐴 / 𝑥⦌{𝑦 ∣ ( 𝐹 “ {𝐵}) = {𝑦}} = ∪ {𝑦 ∣ (⦋𝐴 / 𝑥⦌𝐹 “ {⦋𝐴 / 𝑥⦌𝐵}) = {𝑦}}   )
15:1:	⊢ (   𝐴 ∈ 𝐶   ▶   ⦋𝐴 / 𝑥⦌∪ {𝑦 ∣ ( 𝐹 “ {𝐵}) = {𝑦}} = ∪ ⦋𝐴 / 𝑥⦌{𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}}   )
16:14,15:	⊢ (   𝐴 ∈ 𝐶   ▶   ⦋𝐴 / 𝑥⦌∪ {𝑦 ∣ ( 𝐹 “ {𝐵}) = {𝑦}} = ∪ {𝑦 ∣ (⦋𝐴 / 𝑥⦌𝐹 “ {⦋𝐴 / 𝑥⦌𝐵}) = {𝑦}}   )
17::	⊢ (𝐹‘𝐵) = ∪ {𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}}
18:17:	⊢ ∀𝑥(𝐹‘𝐵) = ∪ {𝑦 ∣ (𝐹 “ {𝐵 }) = {𝑦}}
19:1,18:	⊢ (   𝐴 ∈ 𝐶   ▶   ⦋𝐴 / 𝑥⦌(𝐹‘𝐵) = ⦋𝐴 / 𝑥⦌∪ {𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}}   )
20:16,19:	⊢ (   𝐴 ∈ 𝐶   ▶   ⦋𝐴 / 𝑥⦌(𝐹‘𝐵) = ∪ {𝑦 ∣ (⦋𝐴 / 𝑥⦌𝐹 “ {⦋𝐴 / 𝑥⦌𝐵}) = {𝑦}}   )
21::	⊢ (⦋𝐴 / 𝑥⦌𝐹‘⦋𝐴 / 𝑥⦌𝐵) = ∪ {𝑦 ∣ (⦋𝐴 / 𝑥⦌𝐹 “ {⦋𝐴 / 𝑥⦌𝐵}) = {𝑦}}
22:20,21:	⊢ (   𝐴 ∈ 𝐶   ▶   ⦋𝐴 / 𝑥⦌(𝐹‘𝐵) = (⦋𝐴 / 𝑥⦌𝐹‘⦋𝐴 / 𝑥⦌𝐵)   )
qed:22:	⊢ (𝐴 ∈ 𝐶 → ⦋𝐴 / 𝑥⦌(𝐹‘𝐵) = (⦋𝐴 / 𝑥⦌𝐹‘⦋𝐴 / 𝑥⦌𝐵))

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

⊢ (𝐴 ∈ 𝐶 → ⦋𝐴 / 𝑥⦌(𝐹‘𝐵) = (⦋𝐴 / 𝑥⦌𝐹‘⦋𝐴 / 𝑥⦌𝐵))

Theorem

con5VD 45016

Virtual deduction proof of con5 44639. 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. con5 44639 is con5VD 45016 without virtual deductions and was automatically derived from con5VD 45016.

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

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

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

Theorem

relopabVD 45017

Virtual deduction proof of relopab 5768. 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. relopab 5768 is relopabVD 45017 without virtual deductions and was automatically derived from relopabVD 45017.

1::	⊢ (   𝑦 = 𝑣   ▶   𝑦 = 𝑣   )
2:1:	⊢ (   𝑦 = 𝑣   ▶   ⟨𝑥   ,   𝑦⟩ = ⟨𝑥   ,   𝑣 ⟩   )
3::	⊢ (   𝑦 = 𝑣   ,   𝑥 = 𝑢   ▶   𝑥 = 𝑢   )
4:3:	⊢ (   𝑦 = 𝑣   ,   𝑥 = 𝑢   ▶   ⟨𝑥   ,   𝑣⟩ = ⟨ 𝑢, 𝑣⟩   )
5:2,4:	⊢ (   𝑦 = 𝑣   ,   𝑥 = 𝑢   ▶   ⟨𝑥   ,   𝑦⟩ = ⟨ 𝑢, 𝑣⟩   )
6:5:	⊢ (   𝑦 = 𝑣   ,   𝑥 = 𝑢   ▶   (𝑧 = ⟨𝑥   ,   𝑦 ⟩ → 𝑧 = ⟨𝑢, 𝑣⟩)   )
7:6:	⊢ (   𝑦 = 𝑣   ▶   (𝑥 = 𝑢 → (𝑧 = ⟨𝑥   ,    𝑦⟩ → 𝑧 = ⟨𝑢, 𝑣⟩))   )
8:7:	⊢ (𝑦 = 𝑣 → (𝑥 = 𝑢 → (𝑧 = ⟨𝑥   ,   𝑦 ⟩ → 𝑧 = ⟨𝑢, 𝑣⟩)))
9:8:	⊢ (∃𝑣𝑦 = 𝑣 → ∃𝑣(𝑥 = 𝑢 → (𝑧 = ⟨𝑥, 𝑦⟩ → 𝑧 = ⟨𝑢, 𝑣⟩)))
90::	⊢ (𝑣 = 𝑦 ↔ 𝑦 = 𝑣)
91:90:	⊢ (∃𝑣𝑣 = 𝑦 ↔ ∃𝑣𝑦 = 𝑣)
92::	⊢ ∃𝑣𝑣 = 𝑦
10:91,92:	⊢ ∃𝑣𝑦 = 𝑣
11:9,10:	⊢ ∃𝑣(𝑥 = 𝑢 → (𝑧 = ⟨𝑥   ,   𝑦⟩ → 𝑧 = ⟨𝑢, 𝑣⟩))
12:11:	⊢ (𝑥 = 𝑢 → ∃𝑣(𝑧 = ⟨𝑥   ,   𝑦⟩ → 𝑧 = ⟨𝑢, 𝑣⟩))
13::	⊢ (∃𝑣(𝑧 = ⟨𝑥   ,   𝑦⟩ → 𝑧 = ⟨𝑢 , 𝑣⟩) → (𝑧 = ⟨𝑥, 𝑦⟩ → ∃𝑣𝑧 = ⟨𝑢, 𝑣⟩))
14:12,13:	⊢ (𝑥 = 𝑢 → (𝑧 = ⟨𝑥   ,   𝑦⟩ → ∃𝑣 𝑧 = ⟨𝑢, 𝑣⟩))
15:14:	⊢ (∃𝑢𝑥 = 𝑢 → ∃𝑢(𝑧 = ⟨𝑥   ,   𝑦 ⟩ → ∃𝑣𝑧 = ⟨𝑢, 𝑣⟩))
150::	⊢ (𝑢 = 𝑥 ↔ 𝑥 = 𝑢)
151:150:	⊢ (∃𝑢𝑢 = 𝑥 ↔ ∃𝑢𝑥 = 𝑢)
152::	⊢ ∃𝑢𝑢 = 𝑥
16:151,152:	⊢ ∃𝑢𝑥 = 𝑢
17:15,16:	⊢ ∃𝑢(𝑧 = ⟨𝑥   ,   𝑦⟩ → ∃𝑣𝑧 = ⟨ 𝑢, 𝑣⟩)
18:17:	⊢ (𝑧 = ⟨𝑥   ,   𝑦⟩ → ∃𝑢∃𝑣𝑧 = ⟨ 𝑢, 𝑣⟩)
19:18:	⊢ (∃𝑦𝑧 = ⟨𝑥   ,   𝑦⟩ → ∃𝑦∃𝑢 ∃𝑣𝑧 = ⟨𝑢, 𝑣⟩)
20::	⊢ (∃𝑦∃𝑢∃𝑣𝑧 = ⟨𝑢   ,   𝑣⟩ → ∃𝑢∃𝑣𝑧 = ⟨𝑢, 𝑣⟩)
21:19,20:	⊢ (∃𝑦𝑧 = ⟨𝑥   ,   𝑦⟩ → ∃𝑢∃𝑣𝑧 = ⟨𝑢, 𝑣⟩)
22:21:	⊢ (∃𝑥∃𝑦𝑧 = ⟨𝑥   ,   𝑦⟩ → ∃𝑥 ∃𝑢∃𝑣𝑧 = ⟨𝑢, 𝑣⟩)
23::	⊢ (∃𝑥∃𝑢∃𝑣𝑧 = ⟨𝑢   ,   𝑣⟩ → ∃𝑢∃𝑣𝑧 = ⟨𝑢, 𝑣⟩)
24:22,23:	⊢ (∃𝑥∃𝑦𝑧 = ⟨𝑥   ,   𝑦⟩ → ∃𝑢 ∃𝑣𝑧 = ⟨𝑢, 𝑣⟩)
25:24:	⊢ {𝑧 ∣ ∃𝑥∃𝑦𝑧 = ⟨𝑥   ,   𝑦⟩} ⊆ {𝑧 ∣ ∃𝑢∃𝑣𝑧 = ⟨𝑢, 𝑣⟩}
26::	⊢ 𝑥 ∈ V
27::	⊢ 𝑦 ∈ V
28:26,27:	⊢ (𝑥 ∈ V ∧ 𝑦 ∈ V)
29:28:	⊢ (𝑧 = ⟨𝑥   ,   𝑦⟩ ↔ (𝑧 = ⟨𝑥   ,   𝑦 ⟩ ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V)))
30:29:	⊢ (∃𝑦𝑧 = ⟨𝑥   ,   𝑦⟩ ↔ ∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V)))
31:30:	⊢ (∃𝑥∃𝑦𝑧 = ⟨𝑥   ,   𝑦⟩ ↔ ∃𝑥 ∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V)))
32:31:	⊢ {𝑧 ∣ ∃𝑥∃𝑦𝑧 = ⟨𝑥   ,   𝑦⟩} = { 𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V))}
320:25,32:	⊢ {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥   ,   𝑦⟩ ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V))} ⊆ {𝑧 ∣ ∃𝑢∃𝑣𝑧 = ⟨𝑢, 𝑣⟩}
33::	⊢ 𝑢 ∈ V
34::	⊢ 𝑣 ∈ V
35:33,34:	⊢ (𝑢 ∈ V ∧ 𝑣 ∈ V)
36:35:	⊢ (𝑧 = ⟨𝑢   ,   𝑣⟩ ↔ (𝑧 = ⟨𝑢   ,   𝑣 ⟩ ∧ (𝑢 ∈ V ∧ 𝑣 ∈ V)))
37:36:	⊢ (∃𝑣𝑧 = ⟨𝑢   ,   𝑣⟩ ↔ ∃𝑣(𝑧 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ V ∧ 𝑣 ∈ V)))
38:37:	⊢ (∃𝑢∃𝑣𝑧 = ⟨𝑢   ,   𝑣⟩ ↔ ∃𝑢 ∃𝑣(𝑧 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ V ∧ 𝑣 ∈ V)))
39:38:	⊢ {𝑧 ∣ ∃𝑢∃𝑣𝑧 = ⟨𝑢   ,   𝑣⟩} = { 𝑧 ∣ ∃𝑢∃𝑣(𝑧 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ V ∧ 𝑣 ∈ V))}
40:320,39:	⊢ {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥   ,   𝑦⟩ ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V))} ⊆ {𝑧 ∣ ∃𝑢∃𝑣(𝑧 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ V ∧ 𝑣 ∈ V))}
41::	⊢ {⟨𝑥   ,   𝑦⟩ ∣ (𝑥 ∈ V ∧ 𝑦 ∈ V )} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V)) }
42::	⊢ {⟨𝑢   ,   𝑣⟩ ∣ (𝑢 ∈ V ∧ 𝑣 ∈ V )} = {𝑧 ∣ ∃𝑢∃𝑣(𝑧 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ V ∧ 𝑣 ∈ V)) }
43:40,41,42:	⊢ {⟨𝑥   ,   𝑦⟩ ∣ (𝑥 ∈ V ∧ 𝑦 ∈ V )} ⊆ {⟨𝑢, 𝑣⟩ ∣ (𝑢 ∈ V ∧ 𝑣 ∈ V)}
44::	⊢ {⟨𝑢   ,   𝑣⟩ ∣ (𝑢 ∈ V ∧ 𝑣 ∈ V )} = (V × V)
45:43,44:	⊢ {⟨𝑥   ,   𝑦⟩ ∣ (𝑥 ∈ V ∧ 𝑦 ∈ V )} ⊆ (V × V)
46:28:	⊢ (𝜑 → (𝑥 ∈ V ∧ 𝑦 ∈ V))
47:46:	⊢ {⟨𝑥   ,   𝑦⟩ ∣ 𝜑} ⊆ {⟨𝑥   ,   𝑦⟩ ∣ (𝑥 ∈ V ∧ 𝑦 ∈ V)}
48:45,47:	⊢ {⟨𝑥   ,   𝑦⟩ ∣ 𝜑} ⊆ (V × V)
qed:48:	⊢ Rel {⟨𝑥   ,   𝑦⟩ ∣ 𝜑}

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

⊢ Rel {⟨𝑥, 𝑦⟩ ∣ 𝜑}

Theorem

19.41rgVD 45018

Virtual deduction proof of 19.41rg 44667. 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. 19.41rg 44667 is 19.41rgVD 45018 without virtual deductions and was automatically derived from 19.41rgVD 45018. (Contributed by Alan Sare, 8-Feb-2014.) (Proof modification is discouraged.) (New usage is discouraged.)

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

⊢ (∀𝑥(𝜓 → ∀𝑥𝜓) → ((∃𝑥𝜑 ∧ 𝜓) → ∃𝑥(𝜑 ∧ 𝜓)))

Theorem

2pm13.193VD 45019

Virtual deduction proof of 2pm13.193 44669. 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. 2pm13.193 44669 is 2pm13.193VD 45019 without virtual deductions and was automatically derived from 2pm13.193VD 45019. (Contributed by Alan Sare, 8-Feb-2014.) (Proof modification is discouraged.) (New usage is discouraged.)

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

⊢ (((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑) ↔ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑))

Theorem

hbimpgVD 45020

Virtual deduction proof of hbimpg 44671. 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. hbimpg 44671 is hbimpgVD 45020 without virtual deductions and was automatically derived from hbimpgVD 45020. (Contributed by Alan Sare, 8-Feb-2014.) (Proof modification is discouraged.) (New usage is discouraged.)

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

⊢ ((∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓)) → ∀𝑥((𝜑 → 𝜓) → ∀𝑥(𝜑 → 𝜓)))

Theorem

hbalgVD 45021

Virtual deduction proof of hbalg 44672. 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 44672 is hbalgVD 45021 without virtual deductions and was automatically derived from hbalgVD 45021. (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 45022

Virtual deduction proof of hbexg 44673. 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 44673 is hbexgVD 45022 without virtual deductions and was automatically derived from hbexgVD 45022. (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 45023*

The following User's Proof is a Virtual Deduction proof (see wvd1 44686) completed automatically by a Metamath tools program invoking mmj2 and the Metamath Proof Assistant. ax6e2eq 44674 is ax6e2eqVD 45023 without virtual deductions and was automatically derived from ax6e2eqVD 45023. (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 45024*

The following User's Proof is a Virtual Deduction proof (see wvd1 44686) completed automatically by a Metamath tools program invoking mmj2 and the Metamath Proof Assistant. ax6e2nd 44675 is ax6e2ndVD 45024 without virtual deductions and was automatically derived from ax6e2ndVD 45024. (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 45025*

The following User's Proof is a Virtual Deduction proof (see wvd1 44686) completed automatically by a Metamath tools program invoking mmj2 and the Metamath Proof Assistant. ax6e2eq 44674 is ax6e2ndeqVD 45025 without virtual deductions and was automatically derived from ax6e2ndeqVD 45025. (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 45026*

The following User's Proof is a Virtual Deduction proof (see wvd1 44686) completed automatically by a Metamath tools program invoking mmj2 and the Metamath Proof Assistant. 2sb5nd 44677 is 2sb5ndVD 45026 without virtual deductions and was automatically derived from 2sb5ndVD 45026. (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 45027*

The following User's Proof is a Virtual Deduction proof (see wvd1 44686) completed automatically by a Metamath tools program invoking mmj2 and the Metamath Proof Assistant. 2uasbanh 44678 is 2uasbanhVD 45027 without virtual deductions and was automatically derived from 2uasbanhVD 45027. (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 45028

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

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 45029*

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 2280, 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 44642 is sb5ALTVD 45029 without virtual deductions and was automatically derived from sb5ALTVD 45029.

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 45030

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 44645 is vk15.4jVD 45030 without virtual deductions and was automatically derived from vk15.4jVD 45030. 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 45031

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 44646 is notnotrALTVD 45031 without virtual deductions and was automatically derived from notnotrALTVD 45031. 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 45032

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 44647 is con3ALTVD 45032 without virtual deductions and was automatically derived from con3ALTVD 45032. 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 45033

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

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

Theorem

sspwimp 45034

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 5392. The proof sspwimp 45034, using conventional notation, was translated from virtual deduction form, sspwimpVD 45035, using a translation program. (Contributed by Alan Sare, 23-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (𝐴 ⊆ 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵)

Theorem

sspwimpVD 45035

The following User's Proof is a Virtual Deduction proof (see wvd1 44686) 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 45034 is sspwimpVD 45035 without virtual deductions and was derived from sspwimpVD 45035. (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 45036

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 45036, using conventional notation, was translated from its virtual deduction form, sspwimpcfVD 45037, using a translation program. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (𝐴 ⊆ 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵)

Theorem

sspwimpcfVD 45037

The following User's Proof is a Virtual Deduction proof (see wvd1 44686) 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 45036 is sspwimpcfVD 45037 without virtual deductions and was derived from sspwimpcfVD 45037. 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 45038

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

⊢ (Tr 𝐴 → Tr suc 𝐴)

Theorem

suctrALTcfVD 45039

The following User's Proof is a Virtual Deduction proof (see wvd1 44686) 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 45038 is suctrALTcfVD 45039 without virtual deductions and was derived automatically from suctrALTcfVD 45039. 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 45040

The successor of a transitive class is transitive. suctrALT3 45040 is the completed proof in conventional notation of the Virtual Deduction proof https://us.metamath.org/other/completeusersproof/suctralt3vd.html 45040. It was completed manually. The potential for automated derivation from the VD proof exists. See wvd1 44686 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 44683). 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 5202) . (Contributed by Alan Sare, 3-Dec-2015.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (Tr 𝐴 → Tr suc 𝐴)

Theorem

sspwimpALT 45041

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 45041 is the completed proof in conventional notation of the Virtual Deduction proof https://us.metamath.org/other/completeusersproof/sspwimpaltvd.html 45041. It was completed manually. The potential for automated derivation from the VD proof exists. See wvd1 44686 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 44681). 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 4556). (Contributed by Alan Sare, 3-Dec-2015.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (𝐴 ⊆ 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵)

Theorem

unisnALT 45042

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 45042 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 45042. 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 45042, 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 45043

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 45044

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 45045

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 45028. (Contributed by Alan Sare, 11-Sep-2016.) (Proof modification is discouraged.) (New usage is discouraged.)

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

Theorem

ax6e2ndALT 45046*

If at least two sets exist (dtru 5381), then the same is true expressed in an alternate form similar to the form of ax6e 2385. 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 45024. (Contributed by Alan Sare, 11-Sep-2016.) (Proof modification is discouraged.) (New usage is discouraged.)

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

Theorem

ax6e2ndeqALT 45047*

"At least two sets exist" expressed in the form of dtru 5381 is logically equivalent to the same expressed in a form similar to ax6e 2385 if dtru 5381 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 45025. (Contributed by Alan Sare, 11-Sep-2016.) (Proof modification is discouraged.) (New usage is discouraged.)

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

Theorem

2sb5ndALT 45048*

Equivalence for double substitution 2sb5 2282 without distinct 𝑥, 𝑦 requirement. 2sb5nd 44677 is derived from 2sb5ndVD 45026. 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 45026. (Contributed by Alan Sare, 19-Sep-2016.) (Proof modification is discouraged.) (New usage is discouraged.)

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

Theorem

chordthmALT 45049*

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 26774 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 26775. https://us.metamath.org/other/completeusersproof/chordthmaltvd.html 26775 is a Virtual Deduction User's Proof transcription of chordthm 26775. That VD User's Proof was input into completeusersproof, automatically generating this chordthmALT 45049 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 45050

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

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

Theorem

iunconnlem2 45051*

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 45051 verifies https://us.metamath.org/other/completeusersproof/iunconlem2vd.html 45051. (Contributed by Alan Sare, 22-Apr-2018.) (Proof modification is discouraged.) (New usage is discouraged.)

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

Theorem

iunconnALT 45052*

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 45052 verifies https://us.metamath.org/other/completeusersproof/iunconaltvd.html 45052. (Contributed by Alan Sare, 22-Apr-2018.) (Proof modification is discouraged.) (New usage is discouraged.)

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

Theorem

sineq0ALT 45053

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 45053. The Virtual Deduction proof is based on Mario Carneiro's revision of Norm Megill's proof of sineq0 26461. 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 26461 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 45054*

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

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

Theorem

rext0 45055*

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

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

21.42.2  Study of dfbi1ALT

Theorem

dfbi1ALTa 45056

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 45057

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

⊢ ¬ (𝜑 → ¬ 𝜓)    ⇒   ⊢ 𝜓

Theorem

dfbi1ALTb 45058

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

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

21.42.3  Relation-preserving functions

Syntax

wrelp 45059

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

wff 𝐻 RelPres 𝑅, 𝑆(𝐴, 𝐵)

Definition

df-relp 45060*

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

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

Theorem

relpeq1 45061

Equality theorem for relation-preserving functions. (Contributed by Eric Schmidt, 11-Oct-2025.)

⊢ (𝐻 = 𝐺 → (𝐻 RelPres 𝑅, 𝑆(𝐴, 𝐵) ↔ 𝐺 RelPres 𝑅, 𝑆(𝐴, 𝐵)))

Theorem

relpeq2 45062

Equality theorem for relation-preserving functions. (Contributed by Eric Schmidt, 11-Oct-2025.)

⊢ (𝑅 = 𝑇 → (𝐻 RelPres 𝑅, 𝑆(𝐴, 𝐵) ↔ 𝐻 RelPres 𝑇, 𝑆(𝐴, 𝐵)))

Theorem

relpeq3 45063

Equality theorem for relation-preserving functions. (Contributed by Eric Schmidt, 11-Oct-2025.)

⊢ (𝑆 = 𝑇 → (𝐻 RelPres 𝑅, 𝑆(𝐴, 𝐵) ↔ 𝐻 RelPres 𝑅, 𝑇(𝐴, 𝐵)))

Theorem

relpeq4 45064

Equality theorem for relation-preserving functions. (Contributed by Eric Schmidt, 11-Oct-2025.)

⊢ (𝐴 = 𝐶 → (𝐻 RelPres 𝑅, 𝑆(𝐴, 𝐵) ↔ 𝐻 RelPres 𝑅, 𝑆(𝐶, 𝐵)))

Theorem

relpeq5 45065

Equality theorem for relation-preserving functions. (Contributed by Eric Schmidt, 11-Oct-2025.)

⊢ (𝐵 = 𝐶 → (𝐻 RelPres 𝑅, 𝑆(𝐴, 𝐵) ↔ 𝐻 RelPres 𝑅, 𝑆(𝐴, 𝐶)))

Theorem

nfrelp 45066

Bound-variable hypothesis builder for a relation-preserving function. (Contributed by Eric Schmidt, 11-Oct-2025.)

⊢ Ⅎ𝑥𝐻    &   ⊢ Ⅎ𝑥𝑅    &   ⊢ Ⅎ𝑥𝑆    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥 𝐻 RelPres 𝑅, 𝑆(𝐴, 𝐵)

Theorem

relpf 45067

A relation-preserving function is a function. (Contributed by Eric Schmidt, 11-Oct-2025.)

⊢ (𝐻 RelPres 𝑅, 𝑆(𝐴, 𝐵) → 𝐻:𝐴⟶𝐵)

Theorem

relprel 45068

A relation-preserving function preserves the relation. (Contributed by Eric Schmidt, 11-Oct-2025.)

⊢ ((𝐻 RelPres 𝑅, 𝑆(𝐴, 𝐵) ∧ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → (𝐶𝑅𝐷 → (𝐻‘𝐶)𝑆(𝐻‘𝐷)))

Theorem

relpmin 45069

A preimage of a minimal element under a relation-preserving function is minimal. Essentially one half of isomin 7277. (Contributed by Eric Schmidt, 11-Oct-2025.)

⊢ ((𝐻 RelPres 𝑅, 𝑆(𝐴, 𝐵) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ∈ 𝐴)) → (((𝐻 “ 𝐶) ∩ (^◡𝑆 “ {(𝐻‘𝐷)})) = ∅ → (𝐶 ∩ (^◡𝑅 “ {𝐷})) = ∅))

Theorem

relpfrlem 45070*

Lemma for relpfr 45071. Proved without using the Axiom of Replacement. This is isofrlem 7280 with weaker hypotheses. (Contributed by Eric Schmidt, 11-Oct-2025.)

⊢ (𝜑 → 𝐻 RelPres 𝑅, 𝑆(𝐴, 𝐵))    &   ⊢ (𝜑 → (𝐻 “ 𝑥) ∈ V)    ⇒   ⊢ (𝜑 → (𝑆 Fr 𝐵 → 𝑅 Fr 𝐴))

Theorem

relpfr 45071

If the image of a set under a relation-preserving function is well-founded, so is the set. See isofr 7282 for a bidirectional statement. A more general version of Lemma I.9.9 of [Kunen2] p. 47. (Contributed by Eric Schmidt, 11-Oct-2025.)

⊢ (𝐻 RelPres 𝑅, 𝑆(𝐴, 𝐵) → (𝑆 Fr 𝐵 → 𝑅 Fr 𝐴))

21.42.4  Orbits

Theorem

orbitex 45072

Orbits exist. Given a set 𝐴 and a function 𝐹, the orbit of 𝐴 under 𝐹 is the smallest set 𝑍 such that 𝐴 ∈ 𝑍 and 𝑍 is closed under 𝐹. (Contributed by Eric Schmidt, 6-Nov-2025.)

⊢ (rec(𝐹, 𝐴) “ ω) ∈ V

Theorem

orbitinit 45073

A set is contained in its orbit. (Contributed by Eric Schmidt, 6-Nov-2025.)

⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ (rec(𝐹, 𝐴) “ ω))

Theorem

orbitcl 45074

The orbit under a function is closed under the function. (Contributed by Eric Schmidt, 6-Nov-2025.)

⊢ (𝐵 ∈ (rec(𝐹, 𝐴) “ ω) → (𝐹‘𝐵) ∈ (rec(𝐹, 𝐴) “ ω))

Theorem

orbitclmpt 45075

Version of orbitcl 45074 using maps-to notation. (Contributed by Eric Schmidt, 6-Nov-2025.)

⊢ Ⅎ𝑥𝐵    &   ⊢ Ⅎ𝑥𝐷    &   ⊢ 𝑍 = (rec((𝑥 ∈ V ↦ 𝐶), 𝐴) “ ω)    &   ⊢ (𝑥 = 𝐵 → 𝐶 = 𝐷)    ⇒   ⊢ ((𝐵 ∈ 𝑍 ∧ 𝐷 ∈ 𝑉) → 𝐷 ∈ 𝑍)

21.42.5  Well-founded sets

Theorem

trwf 45076

The class of well-founded sets is transitive. (Contributed by Eric Schmidt, 9-Sep-2025.)

⊢ Tr ∪ (𝑅₁ “ On)

Theorem

rankrelp 45077

The rank function preserves ∈. (Contributed by Eric Schmidt, 11-Oct-2025.)

⊢ rank RelPres E , E (∪ (𝑅₁ “ On), On)

Theorem

wffr 45078

The class of well-founded sets is well-founded. Lemma I.9.24(2) of [Kunen2] p. 53. (Contributed by Eric Schmidt, 11-Oct-2025.)

⊢ E Fr ∪ (𝑅₁ “ On)

Theorem

trfr 45079

A transitive class well-founded by ∈ is a subclass of the class of well-founded sets. Part of Lemma I.9.21 of [Kunen2] p. 53. (Contributed by Eric Schmidt, 26-Oct-2025.)

⊢ ((Tr 𝐴 ∧ E Fr 𝐴) → 𝐴 ⊆ ∪ (𝑅₁ “ On))

Theorem

tcfr 45080

A set is well-founded if and only if its transitive closure is well-founded by ∈. This characterization of well-founded sets is that in Definition I.9.20 of [Kunen2] p. 53. (Contributed by Eric Schmidt, 26-Oct-2025.)

⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ ∪ (𝑅₁ “ On) ↔ E Fr (TC‘𝐴))

Theorem

xpwf 45081

The Cartesian product of two well-founded sets is well-founded. (Contributed by Eric Schmidt, 12-Sep-2025.)

⊢ ((𝐴 ∈ ∪ (𝑅₁ “ On) ∧ 𝐵 ∈ ∪ (𝑅₁ “ On)) → (𝐴 × 𝐵) ∈ ∪ (𝑅₁ “ On))

Theorem

dmwf 45082

The domain of a well-founded set is well-founded. (Contributed by Eric Schmidt, 12-Sep-2025.)

⊢ (𝐴 ∈ ∪ (𝑅₁ “ On) → dom 𝐴 ∈ ∪ (𝑅₁ “ On))

Theorem

rnwf 45083

The range of a well-founded set is well-founded. (Contributed by Eric Schmidt, 12-Sep-2025.)

⊢ (𝐴 ∈ ∪ (𝑅₁ “ On) → ran 𝐴 ∈ ∪ (𝑅₁ “ On))

Theorem

relwf 45084

A relation is a well-founded set iff its domain and range are. (Contributed by Eric Schmidt, 29-Sep-2025.)

⊢ (Rel 𝑅 → (𝑅 ∈ ∪ (𝑅₁ “ On) ↔ (dom 𝑅 ∈ ∪ (𝑅₁ “ On) ∧ ran 𝑅 ∈ ∪ (𝑅₁ “ On))))

21.42.6  Absoluteness in transitive models

Theorem

ralabso 45085*

Simplification of restricted quantification in a transitive class. When 𝜑 is quantifier-free, this shows that the formula ∀𝑥 ∈ 𝑦𝜑 is absolute for transitive models, which is a particular case of Lemma I.16.2 of [Kunen2] p. 95. (Contributed by Eric Schmidt, 19-Oct-2025.)

⊢ ((Tr 𝑀 ∧ 𝐴 ∈ 𝑀) → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝑀 (𝑥 ∈ 𝐴 → 𝜑)))

Theorem

rexabso 45086*

Simplification of restricted quantification in a transitive class. When 𝜑 is quantifier-free, this shows that the formula ∃𝑥 ∈ 𝑦𝜑 is absolute for transitive models, which is a particular case of Lemma I.16.2 of [Kunen2] p. 95. (Contributed by Eric Schmidt, 19-Oct-2025.)

⊢ ((Tr 𝑀 ∧ 𝐴 ∈ 𝑀) → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝑀 (𝑥 ∈ 𝐴 ∧ 𝜑)))

Theorem

ralabsod 45087*

Deduction form of ralabso 45085. (Contributed by Eric Schmidt, 19-Oct-2025.)

⊢ (𝜑 → Tr 𝑀)    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ 𝑀) → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝑀 (𝑥 ∈ 𝐴 → 𝜓)))

Theorem

rexabsod 45088*

Deduction form of rexabso 45086. (Contributed by Eric Schmidt, 19-Oct-2025.)

⊢ (𝜑 → Tr 𝑀)    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ 𝑀) → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝑀 (𝑥 ∈ 𝐴 ∧ 𝜓)))

Theorem

ralabsobidv 45089*

Formula-building lemma for proving absoluteness results. (Contributed by Eric Schmidt, 19-Oct-2025.)

⊢ (𝜑 → Tr 𝑀)    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ 𝑀) → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝑀 (𝑥 ∈ 𝐴 → 𝜒)))

Theorem

rexabsobidv 45090*

Formula-building lemma for proving absoluteness results. (Contributed by Eric Schmidt, 19-Oct-2025.)

⊢ (𝜑 → Tr 𝑀)    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ 𝑀) → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝑀 (𝑥 ∈ 𝐴 ∧ 𝜒)))

Theorem

ssabso 45091*

The notion "𝑥 is a subset of 𝑦 " is absolute for transitive models. Compare Example I.16.3 of [Kunen2] p. 96 and the following discussion. (Contributed by Eric Schmidt, 19-Oct-2025.)

⊢ ((Tr 𝑀 ∧ 𝐴 ∈ 𝑀) → (𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝑀 (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)))

Theorem

disjabso 45092*

Disjointness is absolute for transitive models. Compare Example I.16.3 of [Kunen2] p. 96 and the following discussion. (Contributed by Eric Schmidt, 19-Oct-2025.)

⊢ ((Tr 𝑀 ∧ 𝐴 ∈ 𝑀) → ((𝐴 ∩ 𝐵) = ∅ ↔ ∀𝑥 ∈ 𝑀 (𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵)))

Theorem

n0abso 45093*

Nonemptiness is absolute for transitive models. Compare Example I.16.3 of [Kunen2] p. 96 and the following discussion. (Contributed by Eric Schmidt, 19-Oct-2025.)

⊢ ((Tr 𝑀 ∧ 𝐴 ∈ 𝑀) → (𝐴 ≠ ∅ ↔ ∃𝑥 ∈ 𝑀 𝑥 ∈ 𝐴))

21.42.7  Lemmas for showing axioms hold in models

Theorem

traxext 45094*

A transitive class models the Axiom of Extensionality ax-ext 2705. Lemma II.2.4(1) of [Kunen2] p. 111. (Contributed by Eric Schmidt, 11-Sep-2025.)

⊢ (Tr 𝑀 → ∀𝑥 ∈ 𝑀 ∀𝑦 ∈ 𝑀 (∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦) → 𝑥 = 𝑦))

Theorem

modelaxreplem1 45095*

Lemma for modelaxrep 45098. We show that 𝑀 is closed under taking subsets. (Contributed by Eric Schmidt, 29-Sep-2025.)

⊢ (𝜓 → 𝑥 ⊆ 𝑀)    &   ⊢ (𝜓 → ∀𝑓((Fun 𝑓 ∧ dom 𝑓 ∈ 𝑀 ∧ ran 𝑓 ⊆ 𝑀) → ran 𝑓 ∈ 𝑀))    &   ⊢ (𝜓 → ∅ ∈ 𝑀)    &   ⊢ (𝜓 → 𝑥 ∈ 𝑀)    &   ⊢ 𝐴 ⊆ 𝑥    ⇒   ⊢ (𝜓 → 𝐴 ∈ 𝑀)

Theorem

modelaxreplem2 45096*

Lemma for modelaxrep 45098. We define a class 𝐹 and show that the antecedent of Replacement implies that 𝐹 is a function. We use Replacement (in the form of funex 7159) to show that 𝐹 exists. Then we show that, under our hypotheses, the range of 𝐹 is a member of 𝑀. (Contributed by Eric Schmidt, 29-Sep-2025.)

⊢ (𝜓 → 𝑥 ⊆ 𝑀)    &   ⊢ (𝜓 → ∀𝑓((Fun 𝑓 ∧ dom 𝑓 ∈ 𝑀 ∧ ran 𝑓 ⊆ 𝑀) → ran 𝑓 ∈ 𝑀))    &   ⊢ (𝜓 → ∅ ∈ 𝑀)    &   ⊢ (𝜓 → 𝑥 ∈ 𝑀)    &   ⊢ Ⅎ𝑤𝜓    &   ⊢ Ⅎ𝑧𝜓    &   ⊢ Ⅎ𝑧𝐹    &   ⊢ 𝐹 = {⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ 𝑥 ∧ (𝑧 ∈ 𝑀 ∧ ∀𝑦𝜑))}    &   ⊢ (𝜓 → (𝑤 ∈ 𝑀 → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜑 → 𝑧 = 𝑦)))    ⇒   ⊢ (𝜓 → ran 𝐹 ∈ 𝑀)

Theorem

modelaxreplem3 45097*

Lemma for modelaxrep 45098. We show that the consequent of Replacement is satisfied with ran 𝐹 as the value of 𝑦. (Contributed by Eric Schmidt, 29-Sep-2025.)

⊢ (𝜓 → 𝑥 ⊆ 𝑀)    &   ⊢ (𝜓 → ∀𝑓((Fun 𝑓 ∧ dom 𝑓 ∈ 𝑀 ∧ ran 𝑓 ⊆ 𝑀) → ran 𝑓 ∈ 𝑀))    &   ⊢ (𝜓 → ∅ ∈ 𝑀)    &   ⊢ (𝜓 → 𝑥 ∈ 𝑀)    &   ⊢ Ⅎ𝑤𝜓    &   ⊢ Ⅎ𝑧𝜓    &   ⊢ Ⅎ𝑧𝐹    &   ⊢ 𝐹 = {⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ 𝑥 ∧ (𝑧 ∈ 𝑀 ∧ ∀𝑦𝜑))}    &   ⊢ (𝜓 → (𝑤 ∈ 𝑀 → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜑 → 𝑧 = 𝑦)))    ⇒   ⊢ (𝜓 → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦𝜑)))

Theorem

modelaxrep 45098*

Conditions which guarantee that a class models the Axiom of Replacement ax-rep 5219. Similar to Lemma II.2.4(6) of [Kunen2] p. 111. The first two hypotheses are those in Kunen. The reason for the third hypothesis that our version of Replacement is different from Kunen's (which is zfrep6 7893). If we assumed Regularity, we could eliminate this extra hypothesis, since under Regularity, the empty set is a member of every non-empty transitive class.

Note that, to obtain the relativization of an instance of Replacement to 𝑀, the formula ∀𝑦𝜑 would need to be replaced with ∀𝑦 ∈ 𝑀𝜒, where 𝜒 is 𝜑 with all quantifiers relativized to 𝑀. However, we can obtain this by using 𝑦 ∈ 𝑀 ∧ 𝜒 for 𝜑 in this theorem, so it does establish that all instances of Replacement hold in 𝑀. (Contributed by Eric Schmidt, 29-Sep-2025.)

⊢ (𝜓 → Tr 𝑀)    &   ⊢ (𝜓 → ∀𝑓((Fun 𝑓 ∧ dom 𝑓 ∈ 𝑀 ∧ ran 𝑓 ⊆ 𝑀) → ran 𝑓 ∈ 𝑀))    &   ⊢ (𝜓 → ∅ ∈ 𝑀)    ⇒   ⊢ (𝜓 → ∀𝑥 ∈ 𝑀 (∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜑 → 𝑧 = 𝑦) → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦𝜑))))

Theorem

ssclaxsep 45099*

A class that is closed under subsets models the Axiom of Separation ax-sep 5236. Lemma II.2.4(3) of [Kunen2] p. 111.

Note that, to obtain the relativization of an instance of Separation to 𝑀, the formula 𝜑 would need to be replaced with its relativization to 𝑀. However, this new formula is a valid substitution for 𝜑, so this theorem does establish that all instances of Separation hold in 𝑀. (Contributed by Eric Schmidt, 29-Sep-2025.)

⊢ (∀𝑧 ∈ 𝑀 𝒫 𝑧 ⊆ 𝑀 → ∀𝑧 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑥 ∈ 𝑀 (𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑)))

Theorem

0elaxnul 45100*

A class that contains the empty set models the Null Set Axiom ax-nul 5246. (Contributed by Eric Schmidt, 19-Oct-2025.)

⊢ (∅ ∈ 𝑀 → ∃𝑥 ∈ 𝑀 ∀𝑦 ∈ 𝑀 ¬ 𝑦 ∈ 𝑥)