HomeHome Metamath Proof Explorer
Theorem List (p. 382 of 424)
< 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  Metamath Proof Explorer
(1-27159)
  Hilbert Space Explorer  Hilbert Space Explorer
(27160-28684)
  Users' Mathboxes  Users' Mathboxes
(28685-42360)
 

Theorem List for Metamath Proof Explorer - 38101-38200   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremen3lplem2VD 38101* Virtual deduction proof of en3lplem2 8395. (Contributed by Alan Sare, 24-Oct-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
((𝐴𝐵𝐵𝐶𝐶𝐴) → (𝑥 ∈ {𝐴, 𝐵, 𝐶} → ∃𝑦(𝑦 ∈ {𝐴, 𝐵, 𝐶} ∧ 𝑦𝑥)))
 
Theoremen3lpVD 38102 Virtual deduction proof of en3lp 8396. (Contributed by Alan Sare, 24-Oct-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
¬ (𝐴𝐵𝐵𝐶𝐶𝐴)
 
21.30.7  Theorems proved using Virtual Deduction with mmj2 assistance
 
Theoremsimplbi2VD 38103 Virtual deduction proof of simplbi2 653. The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.
h1:: (𝜑 ↔ (𝜓𝜒))
3:1,?: e0a 38020 ((𝜓𝜒) → 𝜑)
qed:3,?: e0a 38020 (𝜓 → (𝜒𝜑))
The proof of simplbi2 653 was automatically derived from it. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
(𝜑 ↔ (𝜓𝜒))       (𝜓 → (𝜒𝜑))
 
Theorem3ornot23VD 38104 Virtual deduction proof of 3ornot23 37736. The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.
1::
(   𝜑 ∧ ¬ 𝜓)   ▶   𝜑 ∧ ¬ 𝜓)   )
2:: (   𝜑 ∧ ¬ 𝜓)   ,   (𝜒𝜑 𝜓)   ▶   (𝜒𝜑𝜓)   )
3:1,?: e1a 37873 (   𝜑 ∧ ¬ 𝜓)   ▶   ¬ 𝜑   )
4:1,?: e1a 37873 (   𝜑 ∧ ¬ 𝜓)   ▶   ¬ 𝜓   )
5:3,4,?: e11 37934 (   𝜑 ∧ ¬ 𝜓)   ▶   ¬ (𝜑 𝜓)   )
6:2,?: e2 37877 (   𝜑 ∧ ¬ 𝜓)   ,   (𝜒𝜑 𝜓)   ▶   (𝜒 ∨ (𝜑𝜓))   )
7:5,6,?: e12 37972 (   𝜑 ∧ ¬ 𝜓)   ,   (𝜒𝜑 𝜓)   ▶   𝜒   )
8:7: (   𝜑 ∧ ¬ 𝜓)   ▶   ((𝜒 𝜑𝜓) → 𝜒)   )
qed:8: ((¬ 𝜑 ∧ ¬ 𝜓) → ((𝜒 𝜑𝜓) → 𝜒))
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
((¬ 𝜑 ∧ ¬ 𝜓) → ((𝜒𝜑𝜓) → 𝜒))
 
Theoremorbi1rVD 38105 Virtual deduction proof of orbi1r 37737. The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.
1:: (   (𝜑𝜓)   ▶   (𝜑𝜓)   )
2:: (   (𝜑𝜓)   ,   (𝜒𝜑)    ▶   (𝜒𝜑)   )
3:2,?: e2 37877 (   (𝜑𝜓)   ,   (𝜒𝜑)    ▶   (𝜑𝜒)   )
4:1,3,?: e12 37972 (   (𝜑𝜓)   ,   (𝜒𝜑)    ▶   (𝜓𝜒)   )
5:4,?: e2 37877 (   (𝜑𝜓)   ,   (𝜒𝜑)    ▶   (𝜒𝜓)   )
6:5: (   (𝜑𝜓)   ▶   ((𝜒𝜑) → (𝜒𝜓))   )
7:: (   (𝜑𝜓)   ,   (𝜒𝜓)    ▶   (𝜒𝜓)   )
8:7,?: e2 37877 (   (𝜑𝜓)   ,   (𝜒𝜓)    ▶   (𝜓𝜒)   )
9:1,8,?: e12 37972 (   (𝜑𝜓)   ,   (𝜒𝜓)    ▶   (𝜑𝜒)   )
10:9,?: e2 37877 (   (𝜑𝜓)   ,   (𝜒𝜓)    ▶   (𝜒𝜑)   )
11:10: (   (𝜑𝜓)   ▶   ((𝜒𝜓) → (𝜒𝜑))   )
12:6,11,?: e11 37934 (   (𝜑𝜓)   ▶   ((𝜒 𝜑) ↔ (𝜒𝜓))   )
qed:12: ((𝜑𝜓) → ((𝜒𝜑) ↔ (𝜒𝜓)))
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
((𝜑𝜓) → ((𝜒𝜑) ↔ (𝜒𝜓)))
 
Theorembitr3VD 38106 Virtual deduction proof of bitr3 341. The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.
1:: (   (𝜑𝜓)   ▶   (𝜑 𝜓)   )
2:1,?: e1a 37873 (   (𝜑𝜓)   ▶   (𝜓 𝜑)   )
3:: (   (𝜑𝜓)   ,   (𝜑𝜒)    ▶   (𝜑𝜒)   )
4:3,?: e2 37877 (   (𝜑𝜓)   ,   (𝜑𝜒)    ▶   (𝜒𝜑)   )
5:2,4,?: e12 37972 (   (𝜑𝜓)   ,   (𝜑𝜒)    ▶   (𝜓𝜒)   )
6:5: (   (𝜑𝜓)   ▶   ((𝜑 𝜒) → (𝜓𝜒))   )
qed:6: ((𝜑𝜓) → ((𝜑𝜒) → (𝜓𝜒)))
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
((𝜑𝜓) → ((𝜑𝜒) → (𝜓𝜒)))
 
Theorem3orbi123VD 38107 Virtual deduction proof of 3orbi123 37738. The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.
1:: (   ((𝜑𝜓) ∧ (𝜒𝜃) ∧ (𝜏𝜂))   ▶   ((𝜑𝜓) ∧ (𝜒𝜃) ∧ (𝜏𝜂))   )
2:1,?: e1a 37873 (   ((𝜑𝜓) ∧ (𝜒𝜃) ∧ (𝜏𝜂))   ▶   (𝜑𝜓)   )
3:1,?: e1a 37873 (   ((𝜑𝜓) ∧ (𝜒𝜃) ∧ (𝜏𝜂))   ▶   (𝜒𝜃)   )
4:1,?: e1a 37873 (   ((𝜑𝜓) ∧ (𝜒𝜃) ∧ (𝜏𝜂))   ▶   (𝜏𝜂)   )
5:2,3,?: e11 37934 (   ((𝜑𝜓) ∧ (𝜒𝜃) ∧ (𝜏𝜂))   ▶   ((𝜑𝜒) ↔ (𝜓𝜃))   )
6:5,4,?: e11 37934 (   ((𝜑𝜓) ∧ (𝜒𝜃) ∧ (𝜏𝜂))   ▶   (((𝜑𝜒) ∨ 𝜏) ↔ ((𝜓𝜃) 𝜂))   )
7:?: (((𝜑𝜒) ∨ 𝜏) ↔ (𝜑 𝜒𝜏))
8:6,7,?: e10 37940 (   ((𝜑𝜓) ∧ (𝜒𝜃) ∧ (𝜏𝜂))   ▶   ((𝜑𝜒𝜏) ↔ ((𝜓𝜃) 𝜂))   )
9:?: (((𝜓𝜃) ∨ 𝜂) ↔ (𝜓𝜃𝜂))
10:8,9,?: e10 37940 (   ((𝜑𝜓) ∧ (𝜒 𝜃) ∧ (𝜏𝜂))   ▶   ((𝜑𝜒𝜏) ↔ (𝜓 𝜃𝜂))   )
qed:10: (((𝜑𝜓) ∧ (𝜒𝜃) ∧ (𝜏𝜂)) → ((𝜑𝜒𝜏) ↔ (𝜓𝜃 𝜂)))
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
(((𝜑𝜓) ∧ (𝜒𝜃) ∧ (𝜏𝜂)) → ((𝜑𝜒𝜏) ↔ (𝜓𝜃𝜂)))
 
Theoremsbc3orgVD 38108 Virtual deduction proof of sbc3orgOLD 37763. The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.
1:: (   𝐴𝐵   ▶   𝐴𝐵   )
2:1,?: e1a 37873 (   𝐴𝐵   ▶   ([𝐴 / 𝑥]((𝜑 𝜓) ∨ 𝜒) ↔ ([𝐴 / 𝑥](𝜑𝜓) [𝐴 / 𝑥]𝜒))   )
3:: (((𝜑𝜓) ∨ 𝜒) ↔ (𝜑 𝜓𝜒))
32:3: 𝑥(((𝜑𝜓) ∨ 𝜒) ↔ (𝜑𝜓𝜒))
33:1,32,?: e10 37940 (   𝐴𝐵   ▶   [𝐴 / 𝑥](((𝜑 𝜓) ∨ 𝜒) ↔ (𝜑𝜓𝜒))   )
4:1,33,?: e11 37934 (   𝐴𝐵   ▶   ([𝐴 / 𝑥]((𝜑 𝜓) ∨ 𝜒) ↔ [𝐴 / 𝑥](𝜑𝜓𝜒))   )
5:2,4,?: e11 37934 (   𝐴𝐵   ▶   ([𝐴 / 𝑥](𝜑 𝜓𝜒) ↔ ([𝐴 / 𝑥](𝜑𝜓) ∨ [𝐴 / 𝑥]𝜒))   )
6:1,?: e1a 37873 (   𝐴𝐵   ▶   ([𝐴 / 𝑥](𝜑 𝜓) ↔ ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓))   )
7:6,?: e1a 37873 (   𝐴𝐵   ▶   (([𝐴 / 𝑥](𝜑 𝜓) ∨ [𝐴 / 𝑥]𝜒) ↔ (([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓) [𝐴 / 𝑥]𝜒))   )
8:5,7,?: e11 37934 (   𝐴𝐵   ▶   ([𝐴 / 𝑥](𝜑 𝜓𝜒) ↔ (([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓) [𝐴 / 𝑥]𝜒))   )
9:?: ((([𝐴 / 𝑥]𝜑 [𝐴 / 𝑥]𝜓) ∨ [𝐴 / 𝑥]𝜒) ↔ ([𝐴 / 𝑥]𝜑 [𝐴 / 𝑥]𝜓[𝐴 / 𝑥]𝜒))
10:8,9,?: e10 37940 (   𝐴𝐵   ▶   ([𝐴 / 𝑥](𝜑 𝜓𝜒) ↔ ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓 [𝐴 / 𝑥]𝜒))   )
qed:10: (𝐴𝐵 → ([𝐴 / 𝑥](𝜑 𝜓𝜒) ↔ ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓 [𝐴 / 𝑥]𝜒)))
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
(𝐴𝐵 → ([𝐴 / 𝑥](𝜑𝜓𝜒) ↔ ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓[𝐴 / 𝑥]𝜒)))
 
Theorem19.21a3con13vVD 38109* Virtual deduction proof of alrim3con13v 37764. The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.
1:: (   (𝜑 → ∀𝑥𝜑)    ▶   (𝜑 → ∀𝑥𝜑)   )
2:: (   (𝜑 → ∀𝑥𝜑)   ,   (𝜓𝜑 𝜒)   ▶   (𝜓𝜑𝜒)   )
3:2,?: e2 37877 (   (𝜑 → ∀𝑥𝜑)   ,   (𝜓 𝜑𝜒)   ▶   𝜓   )
4:2,?: e2 37877 (   (𝜑 → ∀𝑥𝜑)   ,   (𝜓 𝜑𝜒)   ▶   𝜑   )
5:2,?: e2 37877 (   (𝜑 → ∀𝑥𝜑)   ,   (𝜓 𝜑𝜒)   ▶   𝜒   )
6:1,4,?: e12 37972 (   (𝜑 → ∀𝑥𝜑)   ,   (𝜓 𝜑𝜒)   ▶   𝑥𝜑   )
7:3,?: e2 37877 (   (𝜑 → ∀𝑥𝜑)   ,   (𝜓 𝜑𝜒)   ▶   𝑥𝜓   )
8:5,?: e2 37877 (   (𝜑 → ∀𝑥𝜑)   ,   (𝜓 𝜑𝜒)   ▶   𝑥𝜒   )
9:7,6,8,?: e222 37882 (   (𝜑 → ∀𝑥𝜑)   ,   (𝜓 𝜑𝜒)   ▶   (∀𝑥𝜓 ∧ ∀𝑥𝜑 ∧ ∀𝑥𝜒)   )
10:9,?: e2 37877 (   (𝜑 → ∀𝑥𝜑)   ,   (𝜓 𝜑𝜒)   ▶   𝑥(𝜓𝜑𝜒)   )
11:10:in2 (   (𝜑 → ∀𝑥𝜑)   ▶   ((𝜓 𝜑𝜒) → ∀𝑥(𝜓𝜑𝜒))   )
qed:11:in1 ((𝜑 → ∀𝑥𝜑) → ((𝜓 𝜑𝜒) → ∀𝑥(𝜓𝜑𝜒)))
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
((𝜑 → ∀𝑥𝜑) → ((𝜓𝜑𝜒) → ∀𝑥(𝜓𝜑𝜒)))
 
TheoremexbirVD 38110 Virtual deduction proof of exbir 37705. The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.
1:: (   ((𝜑𝜓) → (𝜒𝜃))    ▶   ((𝜑𝜓) → (𝜒𝜃))   )
2:: (   ((𝜑𝜓) → (𝜒𝜃))   ,    (𝜑𝜓)   ▶   (𝜑𝜓)   )
3:: (   ((𝜑𝜓) → (𝜒𝜃))   ,    (𝜑𝜓), 𝜃   ▶   𝜃   )
5:1,2,?: e12 37972 (   ((𝜑𝜓) → (𝜒 𝜃)), (𝜑𝜓)   ▶   (𝜒𝜃)   )
6:3,5,?: e32 38006 (   ((𝜑𝜓) → (𝜒 𝜃)), (𝜑𝜓), 𝜃   ▶   𝜒   )
7:6: (   ((𝜑𝜓) → (𝜒 𝜃)), (𝜑𝜓)   ▶   (𝜃𝜒)   )
8:7: (   ((𝜑𝜓) → (𝜒𝜃))    ▶   ((𝜑𝜓) → (𝜃𝜒))   )
9:8,?: e1a 37873 (   ((𝜑𝜓) → (𝜒 𝜃))   ▶   (𝜑 → (𝜓 → (𝜃𝜒)))   )
qed:9: (((𝜑𝜓) → (𝜒𝜃)) → (𝜑 → (𝜓 → (𝜃𝜒))))
(Contributed by Alan Sare, 13-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
(((𝜑𝜓) → (𝜒𝜃)) → (𝜑 → (𝜓 → (𝜃𝜒))))
 
TheoremexbiriVD 38111 Virtual deduction proof of exbiri 650. The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.
h1:: ((𝜑𝜓) → (𝜒𝜃))
2:: (   𝜑   ▶   𝜑   )
3:: (   𝜑   ,   𝜓   ▶   𝜓   )
4:: (   𝜑   ,   𝜓   ,   𝜃   ▶   𝜃   )
5:2,1,?: e10 37940 (   𝜑   ▶   (𝜓 → (𝜒𝜃))   )
6:3,5,?: e21 37978 (   𝜑   ,   𝜓   ▶   (𝜒𝜃)   )
7:4,6,?: e32 38006 (   𝜑   ,   𝜓   ,   𝜃   ▶   𝜒   )
8:7: (   𝜑   ,   𝜓   ▶   (𝜃𝜒)   )
9:8: (   𝜑   ▶   (𝜓 → (𝜃𝜒))   )
qed:9: (𝜑 → (𝜓 → (𝜃𝜒)))
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
((𝜑𝜓) → (𝜒𝜃))       (𝜑 → (𝜓 → (𝜃𝜒)))
 
Theoremrspsbc2VD 38112* Virtual deduction proof of rspsbc2 37765. The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.
1:: (   𝐴𝐵   ▶   𝐴𝐵   )
2:: (   𝐴𝐵   ,   𝐶𝐷   ▶   𝐶𝐷   )
3:: (   𝐴𝐵   ,   𝐶𝐷   ,   𝑥𝐵 𝑦𝐷𝜑   ▶   𝑥𝐵𝑦𝐷𝜑   )
4:1,3,?: e13 37996 (   𝐴𝐵   ,   𝐶𝐷   ,   𝑥𝐵 𝑦𝐷𝜑   ▶   [𝐴 / 𝑥]𝑦𝐷𝜑   )
5:1,4,?: e13 37996 (   𝐴𝐵   ,   𝐶𝐷   ,   𝑥𝐵 𝑦𝐷𝜑   ▶   𝑦𝐷[𝐴 / 𝑥]𝜑   )
6:2,5,?: e23 38003 (   𝐴𝐵   ,   𝐶𝐷   ,   𝑥𝐵 𝑦𝐷𝜑   ▶   [𝐶 / 𝑦][𝐴 / 𝑥]𝜑   )
7:6: (   𝐴𝐵   ,   𝐶𝐷   ▶   (∀𝑥𝐵 𝑦𝐷𝜑[𝐶 / 𝑦][𝐴 / 𝑥]𝜑)   )
8:7: (   𝐴𝐵   ▶   (𝐶𝐷 → (∀𝑥𝐵𝑦𝐷𝜑[𝐶 / 𝑦][𝐴 / 𝑥]𝜑))   )
qed:8: (𝐴𝐵 → (𝐶𝐷 → (∀𝑥𝐵𝑦𝐷𝜑[𝐶 / 𝑦][𝐴 / 𝑥]𝜑)))
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
(𝐴𝐵 → (𝐶𝐷 → (∀𝑥𝐵𝑦𝐷 𝜑[𝐶 / 𝑦][𝐴 / 𝑥]𝜑)))
 
Theorem3impexpVD 38113 Virtual deduction proof of 3impexp 1281. The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.
1:: (   ((𝜑𝜓𝜒) 𝜃)   ▶   ((𝜑𝜓𝜒) → 𝜃)   )
2:: ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∧ 𝜒))
3:1,2,?: e10 37940 (   ((𝜑𝜓𝜒) 𝜃)   ▶   (((𝜑𝜓) ∧ 𝜒) → 𝜃)   )
4:3,?: e1a 37873 (   ((𝜑𝜓𝜒) 𝜃)   ▶   ((𝜑𝜓) → (𝜒𝜃))   )
5:4,?: e1a 37873 (   ((𝜑𝜓𝜒) 𝜃)   ▶   (𝜑 → (𝜓 → (𝜒𝜃)))   )
6:5: (((𝜑𝜓𝜒) → 𝜃) → (𝜑 → (𝜓 → (𝜒𝜃))))
7:: (   (𝜑 → (𝜓 → (𝜒 𝜃)))   ▶   (𝜑 → (𝜓 → (𝜒𝜃)))   )
8:7,?: e1a 37873 (   (𝜑 → (𝜓 → (𝜒 𝜃)))   ▶   ((𝜑𝜓) → (𝜒𝜃))   )
9:8,?: e1a 37873 (   (𝜑 → (𝜓 → (𝜒 𝜃)))   ▶   (((𝜑𝜓) ∧ 𝜒) → 𝜃)   )
10:2,9,?: e01 37937 (   (𝜑 → (𝜓 → (𝜒 𝜃)))   ▶   ((𝜑𝜓𝜒) → 𝜃)   )
11:10: ((𝜑 → (𝜓 → (𝜒 𝜃))) → ((𝜑𝜓𝜒) → 𝜃))
qed:6,11,?: e00 38016 (((𝜑𝜓𝜒) 𝜃) ↔ (𝜑 → (𝜓 → (𝜒𝜃))))
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
(((𝜑𝜓𝜒) → 𝜃) ↔ (𝜑 → (𝜓 → (𝜒𝜃))))
 
Theorem3impexpbicomVD 38114 Virtual deduction proof of 3impexpbicom 37706. The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.
1:: (   ((𝜑𝜓𝜒) → (𝜃𝜏))   ▶   ((𝜑𝜓𝜒) → (𝜃𝜏))   )
2:: ((𝜃𝜏) ↔ (𝜏 𝜃))
3:1,2,?: e10 37940 (   ((𝜑𝜓𝜒) → (𝜃𝜏))   ▶   ((𝜑𝜓𝜒) → (𝜏𝜃))   )
4:3,?: e1a 37873 (   ((𝜑𝜓𝜒) → (𝜃𝜏))   ▶   (𝜑 → (𝜓 → (𝜒 → (𝜏 𝜃))))   )
5:4: (((𝜑𝜓𝜒) → (𝜃𝜏)) → (𝜑 → (𝜓 → (𝜒 → (𝜏 𝜃)))))
6:: (   (𝜑 → (𝜓 → (𝜒 → (𝜏𝜃))))   ▶   (𝜑 → (𝜓 → (𝜒 → (𝜏 𝜃))))   )
7:6,?: e1a 37873 (   (𝜑 → (𝜓 → (𝜒 → (𝜏𝜃))))   ▶   ((𝜑𝜓𝜒) → (𝜏 𝜃))   )
8:7,2,?: e10 37940 (   (𝜑 → (𝜓 → (𝜒 → (𝜏𝜃))))   ▶   ((𝜑𝜓𝜒) → (𝜃 𝜏))   )
9:8: ((𝜑 → (𝜓 → (𝜒 → (𝜏𝜃)))) → ((𝜑𝜓𝜒) → (𝜃 𝜏)))
qed:5,9,?: e00 38016 (((𝜑𝜓𝜒) → (𝜃𝜏)) ↔ (𝜑 → (𝜓 → (𝜒 → (𝜏 𝜃)))))
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
(((𝜑𝜓𝜒) → (𝜃𝜏)) ↔ (𝜑 → (𝜓 → (𝜒 → (𝜏𝜃)))))
 
Theorem3impexpbicomiVD 38115 Virtual deduction proof of 3impexpbicomi 37707. The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.
h1:: ((𝜑𝜓𝜒) → (𝜃 𝜏))
qed:1,?: e0a 38020 (𝜑 → (𝜓 → (𝜒 → (𝜏𝜃))))
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
((𝜑𝜓𝜒) → (𝜃𝜏))       (𝜑 → (𝜓 → (𝜒 → (𝜏𝜃))))
 
Theoremsbcel1gvOLD 38116* Class substitution into a membership relation. (Contributed by NM, 17-Nov-2006.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) Obsolete as of 17-Aug-2018. Use sbcel1v 3462 instead. (New usage is discouraged.) (Proof modification is discouraged.)
(𝐴𝑉 → ([𝐴 / 𝑥]𝑥𝐵𝐴𝐵))
 
TheoremsbcoreleleqVD 38117* Virtual deduction proof of sbcoreleleq 37766. The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.
1:: (   𝐴𝐵   ▶   𝐴𝐵   )
2:1,?: e1a 37873 (   𝐴𝐵   ▶   ([𝐴 / 𝑦]𝑥 𝑦𝑥𝐴)   )
3:1,?: e1a 37873 (   𝐴𝐵   ▶   ([𝐴 / 𝑦]𝑦 𝑥𝐴𝑥)   )
4:1,?: e1a 37873 (   𝐴𝐵   ▶   ([𝐴 / 𝑦]𝑥 = 𝑦𝑥 = 𝐴)   )
5:2,3,4,?: e111 37920 (   𝐴𝐵   ▶   ((𝑥𝐴 𝐴𝑥𝑥 = 𝐴) ↔ ([𝐴 / 𝑦]𝑥𝑦[𝐴 / 𝑦]𝑦𝑥 [𝐴 / 𝑦]𝑥 = 𝑦))   )
6:1,?: e1a 37873 (   𝐴𝐵    ▶   ([𝐴 / 𝑦](𝑥𝑦𝑦𝑥𝑥 = 𝑦) ↔ ([𝐴 / 𝑦]𝑥 𝑦[𝐴 / 𝑦]𝑦𝑥[𝐴 / 𝑦]𝑥 = 𝑦))   )
7:5,6: e11 37934 (   𝐴𝐵   ▶   ([𝐴 / 𝑦](𝑥 𝑦𝑦𝑥𝑥 = 𝑦) ↔ (𝑥𝐴𝐴𝑥𝑥 = 𝐴))   )
qed:7: (𝐴𝐵 → ([𝐴 / 𝑦](𝑥𝑦 𝑦𝑥𝑥 = 𝑦) ↔ (𝑥𝐴𝐴𝑥𝑥 = 𝐴)))
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
(𝐴𝐵 → ([𝐴 / 𝑦](𝑥𝑦𝑦𝑥𝑥 = 𝑦) ↔ (𝑥𝐴𝐴𝑥𝑥 = 𝐴)))
 
Theoremhbra2VD 38118* Virtual deduction proof of nfra2 2930. The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.
1:: (∀𝑦𝐵𝑥𝐴𝜑 𝑦𝑦𝐵𝑥𝐴𝜑)
2:: (∀𝑥𝐴𝑦𝐵𝜑 𝑦𝐵𝑥𝐴𝜑)
3:1,2,?: e00 38016 (∀𝑥𝐴𝑦𝐵𝜑 𝑦𝑦𝐵𝑥𝐴𝜑)
4:2: 𝑦(∀𝑥𝐴𝑦𝐵𝜑 𝑦𝐵𝑥𝐴𝜑)
5:4,?: e0a 38020 (∀𝑦𝑥𝐴𝑦𝐵𝜑 𝑦𝑦𝐵𝑥𝐴𝜑)
qed:3,5,?: e00 38016 (∀𝑥𝐴𝑦𝐵𝜑 𝑦𝑥𝐴𝑦𝐵𝜑)
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
(∀𝑥𝐴𝑦𝐵 𝜑 → ∀𝑦𝑥𝐴𝑦𝐵 𝜑)
 
TheoremtratrbVD 38119* Virtual deduction proof of tratrb 37767. The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.
1:: (   (Tr 𝐴 ∧ ∀𝑥𝐴 𝑦𝐴(𝑥𝑦𝑦𝑥𝑥 = 𝑦) ∧ 𝐵𝐴)    ▶   (Tr 𝐴 ∧ ∀𝑥𝐴𝑦𝐴(𝑥𝑦𝑦𝑥𝑥 = 𝑦) 𝐵𝐴)   )
2:1,?: e1a 37873 (   (Tr 𝐴 ∧ ∀𝑥𝐴 𝑦𝐴(𝑥𝑦𝑦𝑥𝑥 = 𝑦) ∧ 𝐵𝐴)   ▶   Tr 𝐴   )
3:1,?: e1a 37873 (   (Tr 𝐴 ∧ ∀𝑥𝐴 𝑦𝐴(𝑥𝑦𝑦𝑥𝑥 = 𝑦) ∧ 𝐵𝐴)    ▶   𝑥𝐴𝑦𝐴(𝑥𝑦𝑦𝑥𝑥 = 𝑦)   )
4:1,?: e1a 37873 (   (Tr 𝐴 ∧ ∀𝑥𝐴 𝑦𝐴(𝑥𝑦𝑦𝑥𝑥 = 𝑦) ∧ 𝐵𝐴)   ▶   𝐵𝐴   )
5:: (   (Tr 𝐴 ∧ ∀𝑥𝐴 𝑦𝐴(𝑥𝑦𝑦𝑥𝑥 = 𝑦) ∧ 𝐵𝐴), (𝑥𝑦 𝑦𝐵)   ▶   (𝑥𝑦𝑦𝐵)   )
6:5,?: e2 37877 (   (Tr 𝐴 ∧ ∀𝑥𝐴 𝑦𝐴(𝑥𝑦𝑦𝑥𝑥 = 𝑦) ∧ 𝐵𝐴), (𝑥𝑦 𝑦𝐵)   ▶   𝑥𝑦   )
7:5,?: e2 37877 (   (Tr 𝐴 ∧ ∀𝑥𝐴 𝑦𝐴(𝑥𝑦𝑦𝑥𝑥 = 𝑦) ∧ 𝐵𝐴), (𝑥𝑦 𝑦𝐵)   ▶   𝑦𝐵   )
8:2,7,4,?: e121 37902 (   (Tr 𝐴 ∧ ∀𝑥𝐴 𝑦𝐴(𝑥𝑦𝑦𝑥𝑥 = 𝑦) ∧ 𝐵𝐴), (𝑥𝑦 𝑦𝐵)   ▶   𝑦𝐴   )
9:2,6,8,?: e122 37899 (   (Tr 𝐴 ∧ ∀𝑥𝐴 𝑦𝐴(𝑥𝑦𝑦𝑥𝑥 = 𝑦) ∧ 𝐵𝐴), (𝑥𝑦 𝑦𝐵)   ▶   𝑥𝐴   )
10:: (   (Tr 𝐴 ∧ ∀𝑥𝐴 𝑦𝐴(𝑥𝑦𝑦𝑥𝑥 = 𝑦) ∧ 𝐵𝐴), (𝑥𝑦 𝑦𝐵), 𝐵𝑥   ▶   𝐵𝑥   )
11:6,7,10,?: e223 37881 (   (Tr 𝐴 ∧ ∀𝑥𝐴 𝑦𝐴(𝑥𝑦𝑦𝑥𝑥 = 𝑦) ∧ 𝐵𝐴), (𝑥𝑦 𝑦𝐵), 𝐵𝑥   ▶   (𝑥𝑦𝑦𝐵𝐵𝑥)   )
12:11: (   (Tr 𝐴 ∧ ∀𝑥𝐴 𝑦𝐴(𝑥𝑦𝑦𝑥𝑥 = 𝑦) ∧ 𝐵𝐴), (𝑥𝑦 𝑦𝐵)   ▶   (𝐵𝑥 → (𝑥𝑦𝑦𝐵𝐵𝑥))   )
13:: ¬ (𝑥𝑦𝑦𝐵 𝐵𝑥)
14:12,13,?: e20 37975 (   (Tr 𝐴 ∧ ∀𝑥𝐴 𝑦𝐴(𝑥𝑦𝑦𝑥𝑥 = 𝑦) ∧ 𝐵𝐴), (𝑥𝑦 𝑦𝐵)   ▶   ¬ 𝐵𝑥   )
15:: (   (Tr 𝐴 ∧ ∀𝑥𝐴 𝑦𝐴(𝑥𝑦𝑦𝑥𝑥 = 𝑦) ∧ 𝐵𝐴), (𝑥𝑦 𝑦𝐵), 𝑥 = 𝐵   ▶   𝑥 = 𝐵   )
16:7,15,?: e23 38003 (   (Tr 𝐴 ∧ ∀𝑥𝐴 𝑦𝐴(𝑥𝑦𝑦𝑥𝑥 = 𝑦) ∧ 𝐵𝐴), (𝑥𝑦 𝑦𝐵), 𝑥 = 𝐵   ▶   𝑦𝑥   )
17:6,16,?: e23 38003 (   (Tr 𝐴 ∧ ∀𝑥𝐴 𝑦𝐴(𝑥𝑦𝑦𝑥𝑥 = 𝑦) ∧ 𝐵𝐴), (𝑥𝑦 𝑦𝐵), 𝑥 = 𝐵   ▶   (𝑥𝑦𝑦𝑥)   )
18:17: (   (Tr 𝐴 ∧ ∀𝑥𝐴 𝑦𝐴(𝑥𝑦𝑦𝑥𝑥 = 𝑦) ∧ 𝐵𝐴), (𝑥𝑦 𝑦𝐵)   ▶   (𝑥 = 𝐵 → (𝑥𝑦𝑦𝑥))   )
19:: ¬ (𝑥𝑦𝑦𝑥)
20:18,19,?: e20 37975 (   (Tr 𝐴 ∧ ∀𝑥𝐴 𝑦𝐴(𝑥𝑦𝑦𝑥𝑥 = 𝑦) ∧ 𝐵𝐴), (𝑥𝑦 𝑦𝐵)   ▶   ¬ 𝑥 = 𝐵   )
21:3,?: e1a 37873 (   (Tr 𝐴 ∧ ∀𝑥𝐴 𝑦𝐴(𝑥𝑦𝑦𝑥𝑥 = 𝑦) ∧ 𝐵𝐴)   ▶   𝑦𝐴 𝑥𝐴(𝑥𝑦𝑦𝑥𝑥 = 𝑦)   )
22:21,9,4,?: e121 37902 (   (Tr 𝐴 ∧ ∀𝑥𝐴 𝑦𝐴(𝑥𝑦𝑦𝑥𝑥 = 𝑦) ∧ 𝐵𝐴), (𝑥𝑦 𝑦𝐵)   ▶   [𝑥 / 𝑥][𝐵 / 𝑦](𝑥𝑦𝑦𝑥 𝑥 = 𝑦)   )
23:22,?: e2 37877 (   (Tr 𝐴 ∧ ∀𝑥𝐴 𝑦𝐴(𝑥𝑦𝑦𝑥𝑥 = 𝑦) ∧ 𝐵𝐴), (𝑥𝑦 𝑦𝐵)   ▶   [𝐵 / 𝑦](𝑥𝑦𝑦𝑥𝑥 = 𝑦)   )
24:4,23,?: e12 37972 (   (Tr 𝐴 ∧ ∀𝑥𝐴 𝑦𝐴(𝑥𝑦𝑦𝑥𝑥 = 𝑦) ∧ 𝐵𝐴), (𝑥𝑦 𝑦𝐵)   ▶   (𝑥𝐵𝐵𝑥𝑥 = 𝐵)   )
25:14,20,24,?: e222 37882 (   (Tr 𝐴 ∧ ∀𝑥𝐴 𝑦𝐴(𝑥𝑦𝑦𝑥𝑥 = 𝑦) ∧ 𝐵𝐴), (𝑥𝑦 𝑦𝐵)   ▶   𝑥𝐵   )
26:25: (   (Tr 𝐴 ∧ ∀𝑥𝐴 𝑦𝐴(𝑥𝑦𝑦𝑥𝑥 = 𝑦) ∧ 𝐵𝐴)   ▶   ((𝑥𝑦 𝑦𝐵) → 𝑥𝐵)   )
27:: (∀𝑥𝐴𝑦𝐴(𝑥𝑦 𝑦𝑥𝑥 = 𝑦) → ∀𝑦𝑥𝐴𝑦𝐴(𝑥𝑦 𝑦𝑥𝑥 = 𝑦))
28:27,?: e0a 38020 ((Tr 𝐴 ∧ ∀𝑥𝐴 𝑦𝐴(𝑥𝑦𝑦𝑥𝑥 = 𝑦) ∧ 𝐵𝐴) → ∀𝑦(Tr 𝐴 ∧ ∀𝑥𝐴𝑦𝐴(𝑥𝑦𝑦𝑥 𝑥 = 𝑦) ∧ 𝐵𝐴))
29:28,26: (   (Tr 𝐴 ∧ ∀𝑥𝐴 𝑦𝐴(𝑥𝑦𝑦𝑥𝑥 = 𝑦) ∧ 𝐵𝐴)    ▶   𝑦((𝑥𝑦𝑦𝐵) → 𝑥𝐵)   )
30:: (∀𝑥𝐴𝑦𝐴(𝑥𝑦 𝑦𝑥𝑥 = 𝑦) → ∀𝑥𝑥𝐴𝑦𝐴(𝑥𝑦 𝑦𝑥𝑥 = 𝑦))
31:30,?: e0a 38020 ((Tr 𝐴 ∧ ∀𝑥𝐴 𝑦𝐴(𝑥𝑦𝑦𝑥𝑥 = 𝑦) ∧ 𝐵𝐴) → ∀𝑥(Tr 𝐴 ∧ ∀𝑥𝐴𝑦𝐴(𝑥𝑦𝑦𝑥𝑥 = 𝑦) ∧ 𝐵𝐴))
32:31,29: (   (Tr 𝐴 ∧ ∀𝑥𝐴 𝑦𝐴(𝑥𝑦𝑦𝑥𝑥 = 𝑦) ∧ 𝐵𝐴)   ▶   𝑥 𝑦((𝑥𝑦𝑦𝐵) → 𝑥𝐵)   )
33:32,?: e1a 37873 (   (Tr 𝐴 ∧ ∀𝑥𝐴 𝑦𝐴(𝑥𝑦𝑦𝑥𝑥 = 𝑦) ∧ 𝐵𝐴)   ▶   Tr 𝐵   )
qed:33: ((Tr 𝐴 ∧ ∀𝑥𝐴 𝑦𝐴(𝑥𝑦𝑦𝑥𝑥 = 𝑦) ∧ 𝐵𝐴) → Tr 𝐵)
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
((Tr 𝐴 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑦𝑦𝑥𝑥 = 𝑦) ∧ 𝐵𝐴) → Tr 𝐵)
 
Theoremal2imVD 38120 Virtual deduction proof of al2im 1732. The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.
1:: (   𝑥(𝜑 → (𝜓𝜒))    ▶   𝑥(𝜑 → (𝜓𝜒))   )
2:1,?: e1a 37873 (   𝑥(𝜑 → (𝜓𝜒))    ▶   (∀𝑥𝜑 → ∀𝑥(𝜓𝜒))   )
3:: (∀𝑥(𝜓𝜒) → (∀𝑥𝜓 → ∀𝑥𝜒))
4:2,3,?: e10 37940 (   𝑥(𝜑 → (𝜓𝜒))    ▶   (∀𝑥𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒))   )
qed:4: (∀𝑥(𝜑 → (𝜓𝜒)) → (∀𝑥𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒)))
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
(∀𝑥(𝜑 → (𝜓𝜒)) → (∀𝑥𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒)))
 
Theoremsyl5impVD 38121 Virtual deduction proof of syl5imp 37739. The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.
1:: (   (𝜑 → (𝜓𝜒))   ▶   (𝜑 → (𝜓𝜒))   )
2:1,?: e1a 37873 (   (𝜑 → (𝜓𝜒))   ▶   (𝜓 → (𝜑𝜒))   )
3:: (   (𝜑 → (𝜓𝜒))   ,   (𝜃 𝜓)   ▶   (𝜃𝜓)   )
4:3,2,?: e21 37978 (   (𝜑 → (𝜓𝜒))   ,   (𝜃 𝜓)   ▶   (𝜃 → (𝜑𝜒))   )
5:4,?: e2 37877 (   (𝜑 → (𝜓𝜒))   ,   (𝜃 𝜓)   ▶   (𝜑 → (𝜃𝜒))   )
6:5: (   (𝜑 → (𝜓𝜒))   ▶   ((𝜃 𝜓) → (𝜑 → (𝜃𝜒)))   )
qed:6: ((𝜑 → (𝜓𝜒)) → ((𝜃 𝜓) → (𝜑 → (𝜃𝜒))))
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
((𝜑 → (𝜓𝜒)) → ((𝜃𝜓) → (𝜑 → (𝜃𝜒))))
 
TheoremidiVD 38122 Virtual deduction proof of idiALT 37704. The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.
h1:: 𝜑
qed:1,?: e0a 38020 𝜑
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
𝜑       𝜑
 
TheoremancomstVD 38123 Closed form of ancoms 468. The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.
1:: ((𝜑𝜓) ↔ (𝜓𝜑))
qed:1,?: e0a 38020 (((𝜑𝜓) → 𝜒) ↔ ((𝜓 𝜑) → 𝜒))
The proof of ancomst 467 is derived automatically from it. (Contributed by Alan Sare, 25-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
(((𝜑𝜓) → 𝜒) ↔ ((𝜓𝜑) → 𝜒))
 
Theoremssralv2VD 38124* Quantification restricted to a subclass for two quantifiers. ssralv 3629 for two quantifiers. 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. ssralv2 37758 is ssralv2VD 38124 without virtual deductions and was automatically derived from ssralv2VD 38124.
1:: (   (𝐴𝐵𝐶𝐷)   ▶   (𝐴𝐵 𝐶𝐷)   )
2:: (   (𝐴𝐵𝐶𝐷)   ,   𝑥𝐵 𝑦𝐷𝜑   ▶   𝑥𝐵𝑦𝐷𝜑   )
3:1: (   (𝐴𝐵𝐶𝐷)   ▶   𝐴𝐵   )
4:3,2: (   (𝐴𝐵𝐶𝐷)   ,   𝑥𝐵 𝑦𝐷𝜑   ▶   𝑥𝐴𝑦𝐷𝜑   )
5:4: (   (𝐴𝐵𝐶𝐷)   ,   𝑥𝐵 𝑦𝐷𝜑   ▶   𝑥(𝑥𝐴 → ∀𝑦𝐷𝜑)   )
6:5: (   (𝐴𝐵𝐶𝐷)   ,   𝑥𝐵 𝑦𝐷𝜑   ▶   (𝑥𝐴 → ∀𝑦𝐷𝜑)   )
7:: (   (𝐴𝐵𝐶𝐷)   ,   𝑥𝐵 𝑦𝐷𝜑, 𝑥𝐴   ▶   𝑥𝐴   )
8:7,6: (   (𝐴𝐵𝐶𝐷)   ,   𝑥𝐵 𝑦𝐷𝜑, 𝑥𝐴   ▶   𝑦𝐷𝜑   )
9:1: (   (𝐴𝐵𝐶𝐷)   ▶   𝐶𝐷   )
10:9,8: (   (𝐴𝐵𝐶𝐷)   ,   𝑥𝐵 𝑦𝐷𝜑, 𝑥𝐴   ▶   𝑦𝐶𝜑   )
11:10: (   (𝐴𝐵𝐶𝐷)   ,   𝑥𝐵 𝑦𝐷𝜑   ▶   (𝑥𝐴 → ∀𝑦𝐶𝜑)   )
12:: ((𝐴𝐵𝐶𝐷) → ∀𝑥(𝐴𝐵𝐶𝐷))
13:: (∀𝑥𝐵𝑦𝐷𝜑 → ∀𝑥𝑥𝐵𝑦𝐷𝜑)
14:12,13,11: (   (𝐴𝐵𝐶𝐷)   ,   𝑥𝐵 𝑦𝐷𝜑   ▶   𝑥(𝑥𝐴 → ∀𝑦𝐶𝜑)   )
15:14: (   (𝐴𝐵𝐶𝐷)   ,   𝑥𝐵 𝑦𝐷𝜑   ▶   𝑥𝐴𝑦𝐶𝜑   )
16:15: (   (𝐴𝐵𝐶𝐷)    ▶   (∀𝑥𝐵𝑦𝐷𝜑 → ∀𝑥𝐴𝑦𝐶𝜑)   )
qed:16: ((𝐴𝐵𝐶𝐷) → (∀𝑥𝐵𝑦𝐷𝜑 → ∀𝑥𝐴𝑦𝐶𝜑))
(Contributed by Alan Sare, 10-Feb-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
((𝐴𝐵𝐶𝐷) → (∀𝑥𝐵𝑦𝐷 𝜑 → ∀𝑥𝐴𝑦𝐶 𝜑))
 
TheoremordelordALTVD 38125 An element of an ordinal class is ordinal. Proposition 7.6 of [TakeutiZaring] p. 36. This is an alternate proof of ordelord 5662 using the Axiom of Regularity indirectly through dford2 8400. dford2 is a weaker definition of ordinal number. Given the Axiom of Regularity, it need not be assumed that E Fr 𝐴 because this is inferred by the Axiom of Regularity. 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. ordelordALT 37768 is ordelordALTVD 38125 without virtual deductions and was automatically derived from ordelordALTVD 38125 using the tools program translate..without..overwriting.cmd and Metamath's minimize command.
1:: (   (Ord 𝐴𝐵𝐴)   ▶   (Ord 𝐴 𝐵𝐴)   )
2:1: (   (Ord 𝐴𝐵𝐴)   ▶   Ord 𝐴   )
3:1: (   (Ord 𝐴𝐵𝐴)   ▶   𝐵𝐴   )
4:2: (   (Ord 𝐴𝐵𝐴)   ▶   Tr 𝐴   )
5:2: (   (Ord 𝐴𝐵𝐴)   ▶   𝑥𝐴 𝑦𝐴(𝑥𝑦𝑥 = 𝑦𝑦𝑥)   )
6:4,3: (   (Ord 𝐴𝐵𝐴)   ▶   𝐵𝐴   )
7:6,6,5: (   (Ord 𝐴𝐵𝐴)   ▶   𝑥𝐵 𝑦𝐵(𝑥𝑦𝑥 = 𝑦𝑦𝑥)   )
8:: ((𝑥𝑦𝑥 = 𝑦𝑦𝑥) ↔ (𝑥𝑦𝑦𝑥𝑥 = 𝑦))
9:8: 𝑦((𝑥𝑦𝑥 = 𝑦𝑦𝑥) ↔ (𝑥𝑦𝑦𝑥𝑥 = 𝑦))
10:9: 𝑦𝐴((𝑥𝑦𝑥 = 𝑦 𝑦𝑥) ↔ (𝑥𝑦𝑦𝑥𝑥 = 𝑦))
11:10: (∀𝑦𝐴(𝑥𝑦𝑥 = 𝑦 𝑦𝑥) ↔ ∀𝑦𝐴(𝑥𝑦𝑦𝑥𝑥 = 𝑦))
12:11: 𝑥(∀𝑦𝐴(𝑥𝑦𝑥 = 𝑦 𝑦𝑥) ↔ ∀𝑦𝐴(𝑥𝑦𝑦𝑥𝑥 = 𝑦))
13:12: 𝑥𝐴(∀𝑦𝐴(𝑥𝑦 𝑥 = 𝑦𝑦𝑥) ↔ ∀𝑦𝐴(𝑥𝑦𝑦𝑥𝑥 = 𝑦))
14:13: (∀𝑥𝐴𝑦𝐴(𝑥𝑦 𝑥 = 𝑦𝑦𝑥) ↔ ∀𝑥𝐴𝑦𝐴(𝑥𝑦𝑦𝑥 𝑥 = 𝑦))
15:14,5: (   (Ord 𝐴𝐵𝐴)   ▶   𝑥𝐴 𝑦𝐴(𝑥𝑦𝑦𝑥𝑥 = 𝑦)   )
16:4,15,3: (   (Ord 𝐴𝐵𝐴)   ▶   Tr 𝐵   )
17:16,7: (   (Ord 𝐴𝐵𝐴)   ▶   Ord 𝐵   )
qed:17: ((Ord 𝐴𝐵𝐴) → Ord 𝐵)
(Contributed by Alan Sare, 12-Feb-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
((Ord 𝐴𝐵𝐴) → Ord 𝐵)
 
TheoremequncomVD 38126 If a class equals the union of two other classes, then it equals the union of those two classes commuted. 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. equncom 3720 is equncomVD 38126 without virtual deductions and was automatically derived from equncomVD 38126.
1:: (   𝐴 = (𝐵𝐶)   ▶   𝐴 = (𝐵𝐶)   )
2:: (𝐵𝐶) = (𝐶𝐵)
3:1,2: (   𝐴 = (𝐵𝐶)   ▶   𝐴 = (𝐶𝐵)   )
4:3: (𝐴 = (𝐵𝐶) → 𝐴 = (𝐶𝐵))
5:: (   𝐴 = (𝐶𝐵)   ▶   𝐴 = (𝐶𝐵)   )
6:5,2: (   𝐴 = (𝐶𝐵)   ▶   𝐴 = (𝐵𝐶)   )
7:6: (𝐴 = (𝐶𝐵) → 𝐴 = (𝐵𝐶))
8:4,7: (𝐴 = (𝐵𝐶) ↔ 𝐴 = (𝐶𝐵))
(Contributed by Alan Sare, 17-Feb-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
(𝐴 = (𝐵𝐶) ↔ 𝐴 = (𝐶𝐵))
 
TheoremequncomiVD 38127 Inference form of equncom 3720. 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. equncomi 3721 is equncomiVD 38127 without virtual deductions and was automatically derived from equncomiVD 38127.
h1:: 𝐴 = (𝐵𝐶)
qed:1: 𝐴 = (𝐶𝐵)
(Contributed by Alan Sare, 18-Feb-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
𝐴 = (𝐵𝐶)       𝐴 = (𝐶𝐵)
 
TheoremsucidALTVD 38128 A set belongs to its successor. Alternate proof of sucid 5721. 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. sucidALT 38129 is sucidALTVD 38128 without virtual deductions and was automatically derived from sucidALTVD 38128. This proof illustrates that completeusersproof.cmd will generate a Metamath proof from any User's Proof which is "conventional" in the sense that no step is a virtual deduction, provided that all necessary unification theorems and transformation deductions are in set.mm. completeusersproof.cmd automatically converts such a conventional proof into a Virtual Deduction proof for which each step happens to be a 0-virtual hypothesis virtual deduction. The user does not need to search for reference theorem labels or deduction labels nor does he(she) need to use theorems and deductions which unify with reference theorems and deductions in set.mm. All that is necessary is that each theorem or deduction of the User's Proof unifies with some reference theorem or deduction in set.mm or is a semantic variation of some theorem or deduction which unifies with some reference theorem or deduction in set.mm. The definition of "semantic variation" has not been precisely defined. If it is obvious that a theorem or deduction has the same meaning as another theorem or deduction, then it is a semantic variation of the latter theorem or deduction. For example, step 4 of the User's Proof is a semantic variation of the definition (axiom) suc 𝐴 = (𝐴 ∪ {𝐴}), which unifies with df-suc 5646, a reference definition (axiom) in set.mm. Also, a theorem or deduction is said to be a semantic variation of another theorem or deduction if it is obvious upon cursory inspection that it has the same meaning as a weaker form of the latter theorem or deduction. For example, the deduction Ord 𝐴 infers 𝑥𝐴𝑦𝐴(𝑥𝑦𝑥 = 𝑦𝑦𝑥) is a semantic variation of the theorem (Ord 𝐴 ↔ (Tr 𝐴 ∧ ∀𝑥𝐴 𝑦𝐴(𝑥𝑦𝑥 = 𝑦𝑦𝑥))), which unifies with the set.mm reference definition (axiom) dford2 8400.
h1:: 𝐴 ∈ V
2:1: 𝐴 ∈ {𝐴}
3:2: 𝐴 ∈ ({𝐴} ∪ 𝐴)
4:: suc 𝐴 = ({𝐴} ∪ 𝐴)
qed:3,4: 𝐴 ∈ suc 𝐴
(Contributed by Alan Sare, 18-Feb-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
𝐴 ∈ V       𝐴 ∈ suc 𝐴
 
TheoremsucidALT 38129 A set belongs to its successor. This proof was automatically derived from sucidALTVD 38128 using translatewithout_overwriting.cmd and minimizing. (Contributed by Alan Sare, 18-Feb-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
𝐴 ∈ V       𝐴 ∈ suc 𝐴
 
TheoremsucidVD 38130 A set belongs to its successor. 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. sucid 5721 is sucidVD 38130 without virtual deductions and was automatically derived from sucidVD 38130.
h1:: 𝐴 ∈ V
2:1: 𝐴 ∈ {𝐴}
3:2: 𝐴 ∈ (𝐴 ∪ {𝐴})
4:: suc 𝐴 = (𝐴 ∪ {𝐴})
qed:3,4: 𝐴 ∈ suc 𝐴
(Contributed by Alan Sare, 18-Feb-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
𝐴 ∈ V       𝐴 ∈ suc 𝐴
 
Theoremimbi12VD 38131 Implication form of imbi12i 339. 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. imbi12 335 is imbi12VD 38131 without virtual deductions and was automatically derived from imbi12VD 38131.
1:: (   (𝜑𝜓)   ▶   (𝜑𝜓)   )
2:: (   (𝜑𝜓)   ,   (𝜒𝜃)    ▶   (𝜒𝜃)   )
3:: (   (𝜑𝜓)   ,   (𝜒𝜃)   ,   (𝜑 𝜒)   ▶   (𝜑𝜒)   )
4:1,3: (   (𝜑𝜓)   ,   (𝜒𝜃)   ,   (𝜑 𝜒)   ▶   (𝜓𝜒)   )
5:2,4: (   (𝜑𝜓)   ,   (𝜒𝜃)   ,   (𝜑 𝜒)   ▶   (𝜓𝜃)   )
6:5: (   (𝜑𝜓)   ,   (𝜒𝜃)    ▶   ((𝜑𝜒) → (𝜓𝜃))   )
7:: (   (𝜑𝜓)   ,   (𝜒𝜃)   ,   (𝜓 𝜃)   ▶   (𝜓𝜃)   )
8:1,7: (   (𝜑𝜓)   ,   (𝜒𝜃)   ,   (𝜓 𝜃)   ▶   (𝜑𝜃)   )
9:2,8: (   (𝜑𝜓)   ,   (𝜒𝜃)   ,   (𝜓 𝜃)   ▶   (𝜑𝜒)   )
10:9: (   (𝜑𝜓)   ,   (𝜒𝜃)    ▶   ((𝜓𝜃) → (𝜑𝜒))   )
11:6,10: (   (𝜑𝜓)   ,   (𝜒𝜃)    ▶   ((𝜑𝜒) ↔ (𝜓𝜃))   )
12:11: (   (𝜑𝜓)   ▶   ((𝜒𝜃) → ((𝜑𝜒) ↔ (𝜓𝜃)))   )
qed:12: ((𝜑𝜓) → ((𝜒𝜃) → ((𝜑𝜒) ↔ (𝜓𝜃))))
(Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
((𝜑𝜓) → ((𝜒𝜃) → ((𝜑𝜒) ↔ (𝜓𝜃))))
 
Theoremimbi13VD 38132 Join three logical equivalences to form equivalence of implications. 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. imbi13 37747 is imbi13VD 38132 without virtual deductions and was automatically derived from imbi13VD 38132.
1:: (   (𝜑𝜓)   ▶   (𝜑𝜓)   )
2:: (   (𝜑𝜓)   ,   (𝜒𝜃)    ▶   (𝜒𝜃)   )
3:: (   (𝜑𝜓)   ,   (𝜒𝜃)   ,   (𝜏 𝜂)   ▶   (𝜏𝜂)   )
4:2,3: (   (𝜑𝜓)   ,   (𝜒𝜃)   ,   (𝜏 𝜂)   ▶   ((𝜒𝜏) ↔ (𝜃𝜂))   )
5:1,4: (   (𝜑𝜓)   ,   (𝜒𝜃)   ,   (𝜏 𝜂)   ▶   ((𝜑 → (𝜒𝜏)) ↔ (𝜓 → (𝜃𝜂)))   )
6:5: (   (𝜑𝜓)   ,   (𝜒𝜃)    ▶   ((𝜏𝜂) → ((𝜑 → (𝜒𝜏)) ↔ (𝜓 → (𝜃 𝜂))))   )
7:6: (   (𝜑𝜓)   ▶   ((𝜒𝜃) → ((𝜏𝜂) → ((𝜑 → (𝜒𝜏)) ↔ (𝜓 → (𝜃 𝜂)))))   )
qed:7: ((𝜑𝜓) → ((𝜒𝜃) → ((𝜏𝜂) → ((𝜑 → (𝜒𝜏)) ↔ (𝜓 → (𝜃 𝜂))))))
(Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
((𝜑𝜓) → ((𝜒𝜃) → ((𝜏𝜂) → ((𝜑 → (𝜒𝜏)) ↔ (𝜓 → (𝜃𝜂))))))
 
Theoremsbcim2gVD 38133 Distribution of class substitution over a left-nested implication. Similar to sbcimg 3444. 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. sbcim2g 37769 is sbcim2gVD 38133 without virtual deductions and was automatically derived from sbcim2gVD 38133.
1:: (   𝐴𝐵   ▶   𝐴𝐵   )
2:: (   𝐴𝐵   ,   [𝐴 / 𝑥](𝜑 → (𝜓 𝜒))   ▶   [𝐴 / 𝑥](𝜑 → (𝜓𝜒))   )
3:1,2: (   𝐴𝐵   ,   [𝐴 / 𝑥](𝜑 → (𝜓 𝜒))   ▶   ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥](𝜓𝜒))   )
4:1: (   𝐴𝐵   ▶   ([𝐴 / 𝑥](𝜓𝜒) ↔ ([𝐴 / 𝑥]𝜓[𝐴 / 𝑥]𝜒))   )
5:3,4: (   𝐴𝐵   ,   [𝐴 / 𝑥](𝜑 → (𝜓 𝜒))   ▶   ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓 [𝐴 / 𝑥]𝜒))   )
6:5: (   𝐴𝐵   ▶   ([𝐴 / 𝑥](𝜑 → (𝜓 𝜒)) → ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓 [𝐴 / 𝑥]𝜒)))   )
7:: (   𝐴𝐵   ,   ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓[𝐴 / 𝑥]𝜒))   ▶   ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓[𝐴 / 𝑥]𝜒))   )
8:4,7: (   𝐴𝐵   ,   ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓[𝐴 / 𝑥]𝜒))   ▶   ([𝐴 / 𝑥]𝜑 [𝐴 / 𝑥](𝜓𝜒))   )
9:1: (   𝐴𝐵   ▶   ([𝐴 / 𝑥](𝜑 → (𝜓 𝜒)) ↔ ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥](𝜓𝜒)))   )
10:8,9: (   𝐴𝐵   ,   ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓[𝐴 / 𝑥]𝜒))   ▶   [𝐴 / 𝑥](𝜑 → (𝜓 𝜒))   )
11:10: (   𝐴𝐵   ▶   (([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓[𝐴 / 𝑥]𝜒)) → [𝐴 / 𝑥](𝜑 → (𝜓 𝜒)))   )
12:6,11: (   𝐴𝐵   ▶   ([𝐴 / 𝑥](𝜑 → (𝜓𝜒)) ↔ ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓 [𝐴 / 𝑥]𝜒)))   )
qed:12: (𝐴𝐵 → ([𝐴 / 𝑥](𝜑 → (𝜓 𝜒)) ↔ ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓 [𝐴 / 𝑥]𝜒))))
(Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
(𝐴𝐵 → ([𝐴 / 𝑥](𝜑 → (𝜓𝜒)) ↔ ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓[𝐴 / 𝑥]𝜒))))
 
TheoremsbcbiVD 38134 Implication form of sbcbiiOLD 37762. 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. sbcbi 37770 is sbcbiVD 38134 without virtual deductions and was automatically derived from sbcbiVD 38134.
1:: (   𝐴𝐵   ▶   𝐴𝐵   )
2:: (   𝐴𝐵   ,   𝑥(𝜑𝜓)    ▶   𝑥(𝜑𝜓)   )
3:1,2: (   𝐴𝐵   ,   𝑥(𝜑𝜓)    ▶   [𝐴 / 𝑥](𝜑𝜓)   )
4:1,3: (   𝐴𝐵   ,   𝑥(𝜑𝜓)    ▶   ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓)   )
5:4: (   𝐴𝐵   ▶   (∀𝑥(𝜑𝜓) → ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓))   )
qed:5: (𝐴𝐵 → (∀𝑥(𝜑𝜓) → ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓)))
(Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
(𝐴𝐵 → (∀𝑥(𝜑𝜓) → ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓)))
 
TheoremtrsbcVD 38135* Formula-building inference rule for class substitution, substituting a class variable for the setvar variable of the transitivity predicate. 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. trsbc 37771 is trsbcVD 38135 without virtual deductions and was automatically derived from trsbcVD 38135.
1:: (   𝐴𝐵   ▶   𝐴𝐵   )
2:1: (   𝐴𝐵   ▶   ([𝐴 / 𝑥]𝑧𝑦 𝑧𝑦)   )
3:1: (   𝐴𝐵   ▶   ([𝐴 / 𝑥]𝑦𝑥 𝑦𝐴)   )
4:1: (   𝐴𝐵   ▶   ([𝐴 / 𝑥]𝑧𝑥 𝑧𝐴)   )
5:1,2,3,4: (   𝐴𝐵   ▶   (([𝐴 / 𝑥]𝑧𝑦 → ([𝐴 / 𝑥]𝑦𝑥[𝐴 / 𝑥]𝑧𝑥)) ↔ (𝑧𝑦 → (𝑦𝐴𝑧𝐴)))   )
6:1: (   𝐴𝐵   ▶   ([𝐴 / 𝑥](𝑧𝑦 → (𝑦𝑥𝑧𝑥)) ↔ ([𝐴 / 𝑥]𝑧𝑦 ([𝐴 / 𝑥]𝑦𝑥[𝐴 / 𝑥]𝑧𝑥)))   )
7:5,6: (   𝐴𝐵   ▶   ([𝐴 / 𝑥](𝑧𝑦 → (𝑦𝑥𝑧𝑥)) ↔ (𝑧𝑦 → (𝑦𝐴 𝑧𝐴)))   )
8:: ((𝑧𝑦 → (𝑦𝐴 𝑧𝐴)) ↔ ((𝑧𝑦𝑦𝐴) → 𝑧𝐴))
9:7,8: (   𝐴𝐵   ▶   ([𝐴 / 𝑥](𝑧𝑦 → (𝑦𝑥𝑧𝑥)) ↔ ((𝑧𝑦𝑦𝐴) 𝑧𝐴))   )
10:: ((𝑧𝑦 → (𝑦𝑥 𝑧𝑥)) ↔ ((𝑧𝑦𝑦𝑥) → 𝑧𝑥))
11:10: 𝑥((𝑧𝑦 → (𝑦𝑥 𝑧𝑥)) ↔ ((𝑧𝑦𝑦𝑥) → 𝑧𝑥))
12:1,11: (   𝐴𝐵   ▶   ([𝐴 / 𝑥](𝑧𝑦 → (𝑦𝑥𝑧𝑥)) ↔ [𝐴 / 𝑥]((𝑧𝑦𝑦𝑥) 𝑧𝑥))   )
13:9,12: (   𝐴𝐵   ▶   ([𝐴 / 𝑥]((𝑧𝑦 𝑦𝑥) → 𝑧𝑥) ↔ ((𝑧𝑦𝑦𝐴) 𝑧𝐴))   )
14:13: (   𝐴𝐵   ▶   𝑦([𝐴 / 𝑥]((𝑧 𝑦𝑦𝑥) → 𝑧𝑥) ↔ ((𝑧𝑦𝑦𝐴) 𝑧𝐴))   )
15:14: (   𝐴𝐵   ▶   (∀𝑦[𝐴 / 𝑥]((𝑧 𝑦𝑦𝑥) → 𝑧𝑥) ↔ ∀𝑦((𝑧𝑦𝑦𝐴) 𝑧𝐴))   )
16:1: (   𝐴𝐵   ▶   ([𝐴 / 𝑥]𝑦((𝑧 𝑦𝑦𝑥) → 𝑧𝑥) ↔ ∀𝑦[𝐴 / 𝑥]((𝑧𝑦 𝑦𝑥) → 𝑧𝑥))   )
17:15,16: (   𝐴𝐵   ▶   ([𝐴 / 𝑥]𝑦((𝑧 𝑦𝑦𝑥) → 𝑧𝑥) ↔ ∀𝑦((𝑧𝑦𝑦𝐴) 𝑧𝐴))   )
18:17: (   𝐴𝐵   ▶   𝑧([𝐴 / 𝑥]𝑦(( 𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ ∀𝑦((𝑧𝑦𝑦𝐴) 𝑧𝐴))   )
19:18: (   𝐴𝐵   ▶   (∀𝑧[𝐴 / 𝑥]𝑦(( 𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ ∀𝑧𝑦((𝑧𝑦 𝑦𝐴) → 𝑧𝐴))   )
20:1: (   𝐴𝐵   ▶   ([𝐴 / 𝑥]𝑧𝑦(( 𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ ∀𝑧[𝐴 / 𝑥]𝑦((𝑧 𝑦𝑦𝑥) → 𝑧𝑥))   )
21:19,20: (   𝐴𝐵   ▶   ([𝐴 / 𝑥]𝑧𝑦(( 𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ ∀𝑧𝑦((𝑧𝑦 𝑦𝐴) → 𝑧𝐴))   )
22:: (Tr 𝐴 ↔ ∀𝑧𝑦((𝑧𝑦 𝑦𝐴) → 𝑧𝐴))
23:21,22: (   𝐴𝐵   ▶   ([𝐴 / 𝑥]𝑧𝑦(( 𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ Tr 𝐴)   )
24:: (Tr 𝑥 ↔ ∀𝑧𝑦((𝑧𝑦𝑦 𝑥) → 𝑧𝑥))
25:24: 𝑥(Tr 𝑥 ↔ ∀𝑧𝑦((𝑧𝑦 𝑦𝑥) → 𝑧𝑥))
26:1,25: (   𝐴𝐵   ▶   ([𝐴 / 𝑥]Tr 𝑥 [𝐴 / 𝑥]𝑧𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥))   )
27:23,26: (   𝐴𝐵   ▶   ([𝐴 / 𝑥]Tr 𝑥 ↔ Tr 𝐴)   )
qed:27: (𝐴𝐵 → ([𝐴 / 𝑥]Tr 𝑥 ↔ Tr 𝐴))
(Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
(𝐴𝐵 → ([𝐴 / 𝑥]Tr 𝑥 ↔ Tr 𝐴))
 
TheoremtruniALTVD 38136* The union of a class of transitive sets is transitive. 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. truniALT 37772 is truniALTVD 38136 without virtual deductions and was automatically derived from truniALTVD 38136.
1:: (   𝑥𝐴Tr 𝑥   ▶   𝑥𝐴 Tr 𝑥   )
2:: (   𝑥𝐴Tr 𝑥   ,   (𝑧𝑦 𝑦 𝐴)   ▶   (𝑧𝑦𝑦 𝐴)   )
3:2: (   𝑥𝐴Tr 𝑥   ,   (𝑧𝑦 𝑦 𝐴)   ▶   𝑧𝑦   )
4:2: (   𝑥𝐴Tr 𝑥   ,   (𝑧𝑦 𝑦 𝐴)   ▶   𝑦 𝐴   )
5:4: (   𝑥𝐴Tr 𝑥   ,   (𝑧𝑦 𝑦 𝐴)   ▶   𝑞(𝑦𝑞𝑞𝐴)   )
6:: (   𝑥𝐴Tr 𝑥   ,   (𝑧𝑦 𝑦 𝐴), (𝑦𝑞𝑞𝐴)   ▶   (𝑦𝑞𝑞𝐴)   )
7:6: (   𝑥𝐴Tr 𝑥   ,   (𝑧𝑦 𝑦 𝐴), (𝑦𝑞𝑞𝐴)   ▶   𝑦𝑞   )
8:6: (   𝑥𝐴Tr 𝑥   ,   (𝑧𝑦 𝑦 𝐴), (𝑦𝑞𝑞𝐴)   ▶   𝑞𝐴   )
9:1,8: (   𝑥𝐴Tr 𝑥   ,   (𝑧𝑦 𝑦 𝐴), (𝑦𝑞𝑞𝐴)   ▶   [𝑞 / 𝑥]Tr 𝑥   )
10:8,9: (   𝑥𝐴Tr 𝑥   ,   (𝑧𝑦 𝑦 𝐴), (𝑦𝑞𝑞𝐴)   ▶   Tr 𝑞   )
11:3,7,10: (   𝑥𝐴Tr 𝑥   ,   (𝑧𝑦 𝑦 𝐴), (𝑦𝑞𝑞𝐴)   ▶   𝑧𝑞   )
12:11,8: (   𝑥𝐴Tr 𝑥   ,   (𝑧𝑦 𝑦 𝐴), (𝑦𝑞𝑞𝐴)   ▶   𝑧 𝐴   )
13:12: (   𝑥𝐴Tr 𝑥   ,   (𝑧𝑦 𝑦 𝐴)   ▶   ((𝑦𝑞𝑞𝐴) → 𝑧 𝐴)   )
14:13: (   𝑥𝐴Tr 𝑥   ,   (𝑧𝑦 𝑦 𝐴)   ▶   𝑞((𝑦𝑞𝑞𝐴) → 𝑧 𝐴)   )
15:14: (   𝑥𝐴Tr 𝑥   ,   (𝑧𝑦 𝑦 𝐴)   ▶   (∃𝑞(𝑦𝑞𝑞𝐴) → 𝑧 𝐴)   )
16:5,15: (   𝑥𝐴Tr 𝑥   ,   (𝑧𝑦 𝑦 𝐴)   ▶   𝑧 𝐴   )
17:16: (   𝑥𝐴Tr 𝑥   ▶   ((𝑧𝑦 𝑦 𝐴) → 𝑧 𝐴)   )
18:17: (   𝑥𝐴Tr 𝑥    ▶   𝑧𝑦((𝑧𝑦𝑦 𝐴) → 𝑧 𝐴)   )
19:18: (   𝑥𝐴Tr 𝑥   ▶   Tr 𝐴   )
qed:19: (∀𝑥𝐴Tr 𝑥 → Tr 𝐴)
(Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
(∀𝑥𝐴 Tr 𝑥 → Tr 𝐴)
 
Theoremee33VD 38137 Non-virtual deduction form of e33 37982. 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. ee33 37748 is ee33VD 38137 without virtual deductions and was automatically derived from ee33VD 38137.
h1:: (𝜑 → (𝜓 → (𝜒𝜃)))
h2:: (𝜑 → (𝜓 → (𝜒𝜏)))
h3:: (𝜃 → (𝜏𝜂))
4:1,3: (𝜑 → (𝜓 → (𝜒 → (𝜏𝜂))))
5:4: (𝜏 → (𝜑 → (𝜓 → (𝜒𝜂))))
6:2,5: (𝜑 → (𝜓 → (𝜒 → (𝜑 → (𝜓 → (𝜒𝜂))))))
7:6: (𝜓 → (𝜒 → (𝜑 → (𝜓 → (𝜒 𝜂)))))
8:7: (𝜒 → (𝜑 → (𝜓 → (𝜒𝜂))))
qed:8: (𝜑 → (𝜓 → (𝜒𝜂)))
(Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
(𝜑 → (𝜓 → (𝜒𝜃)))    &   (𝜑 → (𝜓 → (𝜒𝜏)))    &   (𝜃 → (𝜏𝜂))       (𝜑 → (𝜓 → (𝜒𝜂)))
 
TheoremtrintALTVD 38138* The intersection of a class of transitive sets is transitive. Virtual deduction proof of trintALT 38139. 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. trintALT 38139 is trintALTVD 38138 without virtual deductions and was automatically derived from trintALTVD 38138.
1:: (   𝑥𝐴Tr 𝑥   ▶   𝑥𝐴Tr 𝑥   )
2:: (   𝑥𝐴Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ▶   (𝑧𝑦𝑦 𝐴)   )
3:2: (   𝑥𝐴Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ▶   𝑧𝑦   )
4:2: (   𝑥𝐴Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ▶   𝑦 𝐴   )
5:4: (   𝑥𝐴Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ▶   𝑞𝐴𝑦𝑞   )
6:5: (   𝑥𝐴Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ▶   (𝑞𝐴𝑦𝑞)   )
7:: (   𝑥𝐴Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴), 𝑞𝐴   ▶   𝑞𝐴   )
8:7,6: (   𝑥𝐴Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴), 𝑞𝐴   ▶   𝑦𝑞   )
9:7,1: (   𝑥𝐴Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴), 𝑞𝐴   ▶   [𝑞 / 𝑥]Tr 𝑥   )
10:7,9: (   𝑥𝐴Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴), 𝑞𝐴   ▶   Tr 𝑞   )
11:10,3,8: (   𝑥𝐴Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴), 𝑞𝐴   ▶   𝑧𝑞   )
12:11: (   𝑥𝐴Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ▶   (𝑞𝐴𝑧𝑞)   )
13:12: (   𝑥𝐴Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ▶   𝑞(𝑞𝐴𝑧𝑞)   )
14:13: (   𝑥𝐴Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ▶   𝑞𝐴𝑧𝑞   )
15:3,14: (   𝑥𝐴Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ▶   𝑧 𝐴   )
16:15: (   𝑥𝐴Tr 𝑥   ▶   ((𝑧𝑦𝑦 𝐴) → 𝑧 𝐴)   )
17:16: (   𝑥𝐴Tr 𝑥   ▶   𝑧𝑦((𝑧 𝑦𝑦 𝐴) → 𝑧 𝐴)   )
18:17: (   𝑥𝐴Tr 𝑥   ▶   Tr 𝐴   )
qed:18: (∀𝑥𝐴Tr 𝑥 → Tr 𝐴)
(Contributed by Alan Sare, 17-Apr-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
(∀𝑥𝐴 Tr 𝑥 → Tr 𝐴)
 
TheoremtrintALT 38139* The intersection of a class of transitive sets is transitive. Exercise 5(b) of [Enderton] p. 73. trintALT 38139 is an alternate proof of trint 4696. trintALT 38139 is trintALTVD 38138 without virtual deductions and was automatically derived from trintALTVD 38138 using the tools program translate..without..overwriting.cmd and Metamath's minimize command. (Contributed by Alan Sare, 17-Apr-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
(∀𝑥𝐴 Tr 𝑥 → Tr 𝐴)
 
Theoremundif3VD 38140 The first equality of Exercise 13 of [TakeutiZaring] p. 22. Virtual deduction proof of undif3 3847. 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. undif3 3847 is undif3VD 38140 without virtual deductions and was automatically derived from undif3VD 38140.
1:: (𝑥 ∈ (𝐴 ∪ (𝐵𝐶)) ↔ (𝑥𝐴 𝑥 ∈ (𝐵𝐶)))
2:: (𝑥 ∈ (𝐵𝐶) ↔ (𝑥𝐵 ∧ ¬ 𝑥 𝐶))
3:2: ((𝑥𝐴𝑥 ∈ (𝐵𝐶)) ↔ (𝑥 𝐴 ∨ (𝑥𝐵 ∧ ¬ 𝑥𝐶)))
4:1,3: (𝑥 ∈ (𝐴 ∪ (𝐵𝐶)) ↔ (𝑥𝐴 ∨ (𝑥𝐵 ∧ ¬ 𝑥𝐶)))
5:: (   𝑥𝐴   ▶   𝑥𝐴   )
6:5: (   𝑥𝐴   ▶   (𝑥𝐴𝑥𝐵)   )
7:5: (   𝑥𝐴   ▶   𝑥𝐶𝑥𝐴)   )
8:6,7: (   𝑥𝐴   ▶   ((𝑥𝐴𝑥𝐵) ∧ 𝑥𝐶𝑥𝐴))   )
9:8: (𝑥𝐴 → ((𝑥𝐴𝑥𝐵) ∧ ( ¬ 𝑥𝐶𝑥𝐴)))
10:: (   (𝑥𝐵 ∧ ¬ 𝑥𝐶)   ▶   (𝑥𝐵 ∧ ¬ 𝑥𝐶)   )
11:10: (   (𝑥𝐵 ∧ ¬ 𝑥𝐶)   ▶   𝑥𝐵   )
12:10: (   (𝑥𝐵 ∧ ¬ 𝑥𝐶)   ▶   ¬ 𝑥𝐶    )
13:11: (   (𝑥𝐵 ∧ ¬ 𝑥𝐶)   ▶   (𝑥𝐴 𝑥𝐵)   )
14:12: (   (𝑥𝐵 ∧ ¬ 𝑥𝐶)   ▶   𝑥 𝐶𝑥𝐴)   )
15:13,14: (   (𝑥𝐵 ∧ ¬ 𝑥𝐶)   ▶   ((𝑥 𝐴𝑥𝐵) ∧ (¬ 𝑥𝐶𝑥𝐴))   )
16:15: ((𝑥𝐵 ∧ ¬ 𝑥𝐶) → ((𝑥𝐴 𝑥𝐵) ∧ (¬ 𝑥𝐶𝑥𝐴)))
17:9,16: ((𝑥𝐴 ∨ (𝑥𝐵 ∧ ¬ 𝑥𝐶)) → ((𝑥𝐴𝑥𝐵) ∧ (¬ 𝑥𝐶𝑥𝐴)))
18:: (   (𝑥𝐴 ∧ ¬ 𝑥𝐶)   ▶   (𝑥𝐴 ∧ ¬ 𝑥𝐶)   )
19:18: (   (𝑥𝐴 ∧ ¬ 𝑥𝐶)   ▶   𝑥𝐴   )
20:18: (   (𝑥𝐴 ∧ ¬ 𝑥𝐶)   ▶   ¬ 𝑥𝐶    )
21:18: (   (𝑥𝐴 ∧ ¬ 𝑥𝐶)   ▶   (𝑥𝐴 ∨ (𝑥𝐵 ∧ ¬ 𝑥𝐶))   )
22:21: ((𝑥𝐴 ∧ ¬ 𝑥𝐶) → (𝑥𝐴 (𝑥𝐵 ∧ ¬ 𝑥𝐶)))
23:: (   (𝑥𝐴𝑥𝐴)   ▶   (𝑥𝐴 𝑥𝐴)   )
24:23: (   (𝑥𝐴𝑥𝐴)   ▶   𝑥𝐴   )
25:24: (   (𝑥𝐴𝑥𝐴)   ▶   (𝑥𝐴 (𝑥𝐵 ∧ ¬ 𝑥𝐶))   )
26:25: ((𝑥𝐴𝑥𝐴) → (𝑥𝐴 ∨ ( 𝑥𝐵 ∧ ¬ 𝑥𝐶)))
27:10: (   (𝑥𝐵 ∧ ¬ 𝑥𝐶)   ▶   (𝑥𝐴 ∨ (𝑥𝐵 ∧ ¬ 𝑥𝐶))   )
28:27: ((𝑥𝐵 ∧ ¬ 𝑥𝐶) → (𝑥𝐴 (𝑥𝐵 ∧ ¬ 𝑥𝐶)))
29:: (   (𝑥𝐵𝑥𝐴)   ▶   (𝑥𝐵 𝑥𝐴)   )
30:29: (   (𝑥𝐵𝑥𝐴)   ▶   𝑥𝐴   )
31:30: (   (𝑥𝐵𝑥𝐴)   ▶   (𝑥𝐴 (𝑥𝐵 ∧ ¬ 𝑥𝐶))   )
32:31: ((𝑥𝐵𝑥𝐴) → (𝑥𝐴 ∨ ( 𝑥𝐵 ∧ ¬ 𝑥𝐶)))
33:22,26: (((𝑥𝐴 ∧ ¬ 𝑥𝐶) ∨ (𝑥𝐴 𝑥𝐴)) → (𝑥𝐴 ∨ (𝑥𝐵 ∧ ¬ 𝑥𝐶)))
34:28,32: (((𝑥𝐵 ∧ ¬ 𝑥𝐶) ∨ (𝑥𝐵 𝑥𝐴)) → (𝑥𝐴 ∨ (𝑥𝐵 ∧ ¬ 𝑥𝐶)))
35:33,34: ((((𝑥𝐴 ∧ ¬ 𝑥𝐶) ∨ (𝑥 𝐴𝑥𝐴)) ∨ ((𝑥𝐵 ∧ ¬ 𝑥𝐶) ∨ (𝑥𝐵𝑥𝐴))) → (𝑥𝐴 ∨ (𝑥𝐵 ∧ ¬ 𝑥𝐶)))
36:: ((((𝑥𝐴 ∧ ¬ 𝑥𝐶) ∨ (𝑥 𝐴𝑥𝐴)) ∨ ((𝑥𝐵 ∧ ¬ 𝑥𝐶) ∨ (𝑥𝐵𝑥𝐴))) ↔ ((𝑥𝐴𝑥𝐵) ∧ (¬ 𝑥𝐶𝑥𝐴)))
37:36,35: (((𝑥𝐴𝑥𝐵) ∧ (¬ 𝑥𝐶 𝑥𝐴)) → (𝑥𝐴 ∨ (𝑥𝐵 ∧ ¬ 𝑥𝐶)))
38:17,37: ((𝑥𝐴 ∨ (𝑥𝐵 ∧ ¬ 𝑥𝐶)) ↔ ((𝑥𝐴𝑥𝐵) ∧ (¬ 𝑥𝐶𝑥𝐴)))
39:: (𝑥 ∈ (𝐶𝐴) ↔ (𝑥𝐶 ∧ ¬ 𝑥 𝐴))
40:39: 𝑥 ∈ (𝐶𝐴) ↔ ¬ (𝑥𝐶 ¬ 𝑥𝐴))
41:: (¬ (𝑥𝐶 ∧ ¬ 𝑥𝐴) ↔ (¬ 𝑥 𝐶𝑥𝐴))
42:40,41: 𝑥 ∈ (𝐶𝐴) ↔ (¬ 𝑥𝐶𝑥 𝐴))
43:: (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴𝑥𝐵 ))
44:43,42: ((𝑥 ∈ (𝐴𝐵) ∧ ¬ 𝑥 ∈ (𝐶𝐴) ) ↔ ((𝑥𝐴𝑥𝐵) ∧ (¬ 𝑥𝐶𝑥𝐴)))
45:: (𝑥 ∈ ((𝐴𝐵) ∖ (𝐶𝐴)) ↔ ( 𝑥 ∈ (𝐴𝐵) ∧ ¬ 𝑥 ∈ (𝐶𝐴)))
46:45,44: (𝑥 ∈ ((𝐴𝐵) ∖ (𝐶𝐴)) ↔ ( (𝑥𝐴𝑥𝐵) ∧ (¬ 𝑥𝐶𝑥𝐴)))
47:4,38: (𝑥 ∈ (𝐴 ∪ (𝐵𝐶)) ↔ ((𝑥𝐴 𝑥𝐵) ∧ (¬ 𝑥𝐶𝑥𝐴)))
48:46,47: (𝑥 ∈ (𝐴 ∪ (𝐵𝐶)) ↔ 𝑥 ∈ ((𝐴 𝐵) ∖ (𝐶𝐴)))
49:48: 𝑥(𝑥 ∈ (𝐴 ∪ (𝐵𝐶)) ↔ 𝑥 ((𝐴𝐵) ∖ (𝐶𝐴)))
qed:49: (𝐴 ∪ (𝐵𝐶)) = ((𝐴𝐵) ∖ (𝐶 𝐴))
(Contributed by Alan Sare, 17-Apr-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
(𝐴 ∪ (𝐵𝐶)) = ((𝐴𝐵) ∖ (𝐶𝐴))
 
TheoremsbcssgVD 38141 Virtual deduction proof of sbcssg 4035. 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. sbcssg 4035 is sbcssgVD 38141 without virtual deductions and was automatically derived from sbcssgVD 38141.
1:: (   𝐴𝐵   ▶   𝐴𝐵   )
2:1: (   𝐴𝐵   ▶   ([𝐴 / 𝑥]𝑦𝐶𝑦 𝐴 / 𝑥𝐶)   )
3:1: (   𝐴𝐵   ▶   ([𝐴 / 𝑥]𝑦𝐷𝑦 𝐴 / 𝑥𝐷)   )
4:2,3: (   𝐴𝐵   ▶   (([𝐴 / 𝑥]𝑦𝐶 [𝐴 / 𝑥]𝑦𝐷) ↔ (𝑦𝐴 / 𝑥𝐶𝑦𝐴 / 𝑥𝐷 ))   )
5:1: (   𝐴𝐵   ▶   ([𝐴 / 𝑥](𝑦𝐶 𝑦𝐷) ↔ ([𝐴 / 𝑥]𝑦𝐶[𝐴 / 𝑥]𝑦𝐷))   )
6:4,5: (   𝐴𝐵   ▶   ([𝐴 / 𝑥](𝑦𝐶 𝑦𝐷) ↔ (𝑦𝐴 / 𝑥𝐶𝑦𝐴 / 𝑥𝐷))   )
7:6: (   𝐴𝐵   ▶   𝑦([𝐴 / 𝑥](𝑦 𝐶𝑦𝐷) ↔ (𝑦𝐴 / 𝑥𝐶𝑦𝐴 / 𝑥𝐷))   )
8:7: (   𝐴𝐵   ▶   (∀𝑦[𝐴 / 𝑥](𝑦 𝐶𝑦𝐷) ↔ ∀𝑦(𝑦𝐴 / 𝑥𝐶𝑦𝐴 / 𝑥𝐷) )   )
9:1: (   𝐴𝐵   ▶   ([𝐴 / 𝑥]𝑦(𝑦 𝐶𝑦𝐷) ↔ ∀𝑦[𝐴 / 𝑥](𝑦𝐶𝑦𝐷))   )
10:8,9: (   𝐴𝐵   ▶   ([𝐴 / 𝑥]𝑦(𝑦 𝐶𝑦𝐷) ↔ ∀𝑦(𝑦𝐴 / 𝑥𝐶𝑦𝐴 / 𝑥𝐷) )   )
11:: (𝐶𝐷 ↔ ∀𝑦(𝑦𝐶𝑦𝐷))
110:11: 𝑥(𝐶𝐷 ↔ ∀𝑦(𝑦𝐶𝑦 𝐷))
12:1,110: (   𝐴𝐵   ▶   ([𝐴 / 𝑥]𝐶𝐷 [𝐴 / 𝑥]𝑦(𝑦𝐶𝑦𝐷))   )
13:10,12: (   𝐴𝐵   ▶   ([𝐴 / 𝑥]𝐶𝐷 𝑦(𝑦𝐴 / 𝑥𝐶𝑦𝐴 / 𝑥𝐷))   )
14:: (𝐴 / 𝑥𝐶𝐴 / 𝑥𝐷 ↔ ∀ 𝑦(𝑦𝐴 / 𝑥𝐶𝑦𝐴 / 𝑥𝐷))
15:13,14: (   𝐴𝐵   ▶   ([𝐴 / 𝑥]𝐶𝐷 𝐴 / 𝑥𝐶𝐴 / 𝑥𝐷)   )
qed:15: (𝐴𝐵 → ([𝐴 / 𝑥]𝐶𝐷 𝐴 / 𝑥𝐶𝐴 / 𝑥𝐷))
(Contributed by Alan Sare, 22-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
(𝐴𝐵 → ([𝐴 / 𝑥]𝐶𝐷𝐴 / 𝑥𝐶𝐴 / 𝑥𝐷))
 
TheoremcsbingVD 38142 Virtual deduction proof of csbingOLD 38076. 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. csbingOLD 38076 is csbingVD 38142 without virtual deductions and was automatically derived from csbingVD 38142.
1:: (   𝐴𝐵   ▶   𝐴𝐵   )
2:: (𝐶𝐷) = {𝑦 ∣ (𝑦𝐶𝑦𝐷) }
20:2: 𝑥(𝐶𝐷) = {𝑦 ∣ (𝑦𝐶𝑦 𝐷)}
30:1,20: (   𝐴𝐵   ▶   [𝐴 / 𝑥](𝐶𝐷) = {𝑦 ∣ (𝑦𝐶𝑦𝐷)}   )
3:1,30: (   𝐴𝐵   ▶   𝐴 / 𝑥(𝐶𝐷) = 𝐴 / 𝑥{𝑦 ∣ (𝑦𝐶𝑦𝐷)}   )
4:1: (   𝐴𝐵   ▶   𝐴 / 𝑥{𝑦 ∣ (𝑦𝐶 𝑦𝐷)} = {𝑦[𝐴 / 𝑥](𝑦𝐶𝑦𝐷)}   )
5:3,4: (   𝐴𝐵   ▶   𝐴 / 𝑥(𝐶𝐷) = {𝑦[𝐴 / 𝑥](𝑦𝐶𝑦𝐷)}   )
6:1: (   𝐴𝐵   ▶   ([𝐴 / 𝑥]𝑦𝐶𝑦 𝐴 / 𝑥𝐶)   )
7:1: (   𝐴𝐵   ▶   ([𝐴 / 𝑥]𝑦𝐷𝑦 𝐴 / 𝑥𝐷)   )
8:6,7: (   𝐴𝐵   ▶   (([𝐴 / 𝑥]𝑦𝐶 [𝐴 / 𝑥]𝑦𝐷) ↔ (𝑦𝐴 / 𝑥𝐶𝑦𝐴 / 𝑥𝐷) )   )
9:1: (   𝐴𝐵   ▶   ([𝐴 / 𝑥](𝑦𝐶 𝑦𝐷) ↔ ([𝐴 / 𝑥]𝑦𝐶[𝐴 / 𝑥]𝑦𝐷))   )
10:9,8: (   𝐴𝐵   ▶   ([𝐴 / 𝑥](𝑦𝐶 𝑦𝐷) ↔ (𝑦𝐴 / 𝑥𝐶𝑦𝐴 / 𝑥𝐷))   )
11:10: (   𝐴𝐵   ▶   𝑦([𝐴 / 𝑥](𝑦 𝐶𝑦𝐷) ↔ (𝑦𝐴 / 𝑥𝐶𝑦𝐴 / 𝑥𝐷))   )
12:11: (   𝐴𝐵   ▶   {𝑦[𝐴 / 𝑥](𝑦𝐶 𝑦𝐷)} = {𝑦 ∣ (𝑦𝐴 / 𝑥𝐶𝑦𝐴 / 𝑥𝐷)}   )
13:5,12: (   𝐴𝐵   ▶   𝐴 / 𝑥(𝐶𝐷) = {𝑦 ∣ (𝑦𝐴 / 𝑥𝐶𝑦𝐴 / 𝑥𝐷)}   )
14:: (𝐴 / 𝑥𝐶𝐴 / 𝑥𝐷) = { 𝑦 ∣ (𝑦𝐴 / 𝑥𝐶𝑦𝐴 / 𝑥𝐷)}
15:13,14: (   𝐴𝐵   ▶   𝐴 / 𝑥(𝐶𝐷) = (𝐴 / 𝑥𝐶𝐴 / 𝑥𝐷)   )
qed:15: (𝐴𝐵𝐴 / 𝑥(𝐶𝐷) = ( 𝐴 / 𝑥𝐶𝐴 / 𝑥𝐷))
(Contributed by Alan Sare, 22-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
(𝐴𝐵𝐴 / 𝑥(𝐶𝐷) = (𝐴 / 𝑥𝐶𝐴 / 𝑥𝐷))
 
TheoremonfrALTlem5VD 38143* Virtual deduction proof of onfrALTlem5 37778. 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 37778 is onfrALTlem5VD 38143 without virtual deductions and was automatically derived from onfrALTlem5VD 38143.
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.)
([(𝑎𝑥) / 𝑏]((𝑏 ⊆ (𝑎𝑥) ∧ 𝑏 ≠ ∅) → ∃𝑦𝑏 (𝑏𝑦) = ∅) ↔ (((𝑎𝑥) ⊆ (𝑎𝑥) ∧ (𝑎𝑥) ≠ ∅) → ∃𝑦 ∈ (𝑎𝑥)((𝑎𝑥) ∩ 𝑦) = ∅))
 
TheoremonfrALTlem4VD 38144* Virtual deduction proof of onfrALTlem4 37779. 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 37779 is onfrALTlem4VD 38144 without virtual deductions and was automatically derived from onfrALTlem4VD 38144.
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.)
([𝑦 / 𝑥](𝑥𝑎 ∧ (𝑎𝑥) = ∅) ↔ (𝑦𝑎 ∧ (𝑎𝑦) = ∅))
 
TheoremonfrALTlem3VD 38145* Virtual deduction proof of onfrALTlem3 37780. 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 37780 is onfrALTlem3VD 38145 without virtual deductions and was automatically derived from onfrALTlem3VD 38145.
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 ∧ 𝑎 ≠ ∅)   ,   (𝑥𝑎 ∧ ¬ (𝑎𝑥) = ∅)   ▶   𝑦 ∈ (𝑎𝑥)((𝑎𝑥) ∩ 𝑦) = ∅   )
 
Theoremsimplbi2comtVD 38146 Virtual deduction proof of simplbi2comt 654. 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 654 is simplbi2comtVD 38146 without virtual deductions and was automatically derived from simplbi2comtVD 38146.
1:: (   (𝜑 ↔ (𝜓𝜒))   ▶   (𝜑 ↔ ( 𝜓𝜒))   )
2:1: (   (𝜑 ↔ (𝜓𝜒))   ▶   ((𝜓𝜒 ) → 𝜑)   )
3:2: (   (𝜑 ↔ (𝜓𝜒))   ▶   (𝜓 → (𝜒 𝜑))   )
4:3: (   (𝜑 ↔ (𝜓𝜒))   ▶   (𝜒 → (𝜓 𝜑))   )
qed:4: ((𝜑 ↔ (𝜓𝜒)) → (𝜒 → (𝜓 𝜑)))
(Contributed by Alan Sare, 22-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
((𝜑 ↔ (𝜓𝜒)) → (𝜒 → (𝜓𝜑)))
 
TheoremonfrALTlem2VD 38147* Virtual deduction proof of onfrALTlem2 37782. 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 37782 is onfrALTlem2VD 38147 without virtual deductions and was automatically derived from onfrALTlem2VD 38147.
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 ∧ 𝑎 ≠ ∅)   ,   (𝑥𝑎 ∧ ¬ (𝑎𝑥) = ∅)   ▶   𝑦𝑎 (𝑎𝑦) = ∅   )
 
TheoremonfrALTlem1VD 38148* Virtual deduction proof of onfrALTlem1 37784. 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 37784 is onfrALTlem1VD 38148 without virtual deductions and was automatically derived from onfrALTlem1VD 38148.
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 ∧ 𝑎 ≠ ∅)   ,   (𝑥𝑎 ∧ (𝑎𝑥) = ∅)   ▶   𝑦𝑎 (𝑎𝑦) = ∅   )
 
TheoremonfrALTVD 38149 Virtual deduction proof of onfrALT 37785. 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 37785 is onfrALTVD 38149 without virtual deductions and was automatically derived from onfrALTVD 38149.
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
 
Theoremcsbeq2gVD 38150 Virtual deduction proof of csbeq2gOLD 37786. 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. csbeq2gOLD 37786 is csbeq2gVD 38150 without virtual deductions and was automatically derived from csbeq2gVD 38150.
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.)
(𝐴𝑉 → (∀𝑥 𝐵 = 𝐶𝐴 / 𝑥𝐵 = 𝐴 / 𝑥𝐶))
 
TheoremcsbsngVD 38151 Virtual deduction proof of csbsng 4190. 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 4190 is csbsngVD 38151 without virtual deductions and was automatically derived from csbsngVD 38151.
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.)
(𝐴𝑉𝐴 / 𝑥{𝐵} = {𝐴 / 𝑥𝐵})
 
TheoremcsbxpgVD 38152 Virtual deduction proof of csbxpgOLD 38075. 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. csbxpgOLD 38075 is csbxpgVD 38152 without virtual deductions and was automatically derived from csbxpgVD 38152.
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.)
(𝐴𝑉𝐴 / 𝑥(𝐵 × 𝐶) = (𝐴 / 𝑥𝐵 × 𝐴 / 𝑥𝐶))
 
TheoremcsbresgVD 38153 Virtual deduction proof of csbresgOLD 38077. 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. csbresgOLD 38077 is csbresgVD 38153 without virtual deductions and was automatically derived from csbresgVD 38153.
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.)
(𝐴𝑉𝐴 / 𝑥(𝐵𝐶) = (𝐴 / 𝑥𝐵𝐴 / 𝑥𝐶))
 
TheoremcsbrngVD 38154 Virtual deduction proof of csbrngOLD 38078. 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. csbrngOLD 38078 is csbrngVD 38154 without virtual deductions and was automatically derived from csbrngVD 38154.
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 𝐴 / 𝑥𝐵)
 
Theoremcsbima12gALTVD 38155 Virtual deduction proof of csbima12gALTOLD 38079. 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. csbima12gALTOLD 38079 is csbima12gALTVD 38155 without virtual deductions and was automatically derived from csbima12gALTVD 38155.
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.)
(𝐴𝐶𝐴 / 𝑥(𝐹𝐵) = (𝐴 / 𝑥𝐹𝐴 / 𝑥𝐵))
 
TheoremcsbunigVD 38156 Virtual deduction proof of csbunigOLD 38073. 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. csbunigOLD 38073 is csbunigVD 38156 without virtual deductions and was automatically derived from csbunigVD 38156.
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.)
(𝐴𝑉𝐴 / 𝑥 𝐵 = 𝐴 / 𝑥𝐵)
 
Theoremcsbfv12gALTVD 38157 Virtual deduction proof of csbfv12gALTOLD 38074. 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. csbfv12gALTOLD 38074 is csbfv12gALTVD 38157 without virtual deductions and was automatically derived from csbfv12gALTVD 38157.
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.)
(𝐴𝐶𝐴 / 𝑥(𝐹𝐵) = (𝐴 / 𝑥𝐹𝐴 / 𝑥𝐵))
 
Theoremcon5VD 38158 Virtual deduction proof of con5 37749. 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 37749 is con5VD 38158 without virtual deductions and was automatically derived from con5VD 38158.
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.)
((𝜑 ↔ ¬ 𝜓) → (¬ 𝜑𝜓))
 
TheoremrelopabVD 38159 Virtual deduction proof of relopab 5169. 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 5169 is relopabVD 38159 without virtual deductions and was automatically derived from relopabVD 38159.
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 {⟨𝑥, 𝑦⟩ ∣ 𝜑}
 
Theorem19.41rgVD 38160 Virtual deduction proof of 19.41rg 37787. 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 37787 is 19.41rgVD 38160 without virtual deductions and was automatically derived from 19.41rgVD 38160. (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: (∀𝑥(𝜓 → ∀𝑥𝜓) → ((∃𝑥𝜑 𝜓) → ∃𝑥(𝜑𝜓)))
(∀𝑥(𝜓 → ∀𝑥𝜓) → ((∃𝑥𝜑𝜓) → ∃𝑥(𝜑𝜓)))
 
Theorem2pm13.193VD 38161 Virtual deduction proof of 2pm13.193 37789. 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 37789 is 2pm13.193VD 38161 without virtual deductions and was automatically derived from 2pm13.193VD 38161. (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: (((𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑) ↔ ((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑))
(((𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑) ↔ ((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑))
 
TheoremhbimpgVD 38162 Virtual deduction proof of hbimpg 37791. 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 37791 is hbimpgVD 38162 without virtual deductions and was automatically derived from hbimpgVD 38162. (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: ((∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓)) → ∀𝑥((𝜑𝜓) → ∀𝑥(𝜑𝜓)))
((∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓)) → ∀𝑥((𝜑𝜓) → ∀𝑥(𝜑𝜓)))
 
TheoremhbalgVD 38163 Virtual deduction proof of hbalg 37792. 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 37792 is hbalgVD 38163 without virtual deductions and was automatically derived from hbalgVD 38163. (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: (∀𝑦(𝜑 → ∀𝑥𝜑) → ∀𝑦(∀𝑦 𝜑 → ∀𝑥𝑦𝜑))
(∀𝑦(𝜑 → ∀𝑥𝜑) → ∀𝑦(∀𝑦𝜑 → ∀𝑥𝑦𝜑))
 
TheoremhbexgVD 38164 Virtual deduction proof of hbexg 37793. 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 37793 is hbexgVD 38164 without virtual deductions and was automatically derived from hbexgVD 38164. (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: (   𝑥𝑦(𝜑 → ∀𝑥𝜑)   ▶   𝑥 𝑦(∃𝑦𝜑 → ∀𝑥𝑦𝜑)   )
(∀𝑥𝑦(𝜑 → ∀𝑥𝜑) → ∀𝑥𝑦(∃𝑦𝜑 → ∀𝑥𝑦𝜑))
 
Theoremax6e2eqVD 38165* The following User's Proof is a Virtual Deduction proof (see wvd1 37806) completed automatically by a Metamath tools program invoking mmj2 and the Metamath Proof Assistant. ax6e2eq 37794 is ax6e2eqVD 38165 without virtual deductions and was automatically derived from ax6e2eqVD 38165. (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: (∀𝑥𝑥 = 𝑦 → (𝑢 = 𝑣 → ∃𝑥𝑦( 𝑥 = 𝑢𝑦 = 𝑣)))
(∀𝑥 𝑥 = 𝑦 → (𝑢 = 𝑣 → ∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣)))
 
Theoremax6e2ndVD 38166* The following User's Proof is a Virtual Deduction proof (see wvd1 37806) completed automatically by a Metamath tools program invoking mmj2 and the Metamath Proof Assistant. ax6e2nd 37795 is ax6e2ndVD 38166 without virtual deductions and was automatically derived from ax6e2ndVD 38166. (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: (¬ ∀𝑥𝑥 = 𝑦 → ∃𝑥𝑦(𝑥 = 𝑢 𝑦 = 𝑣))
(¬ ∀𝑥 𝑥 = 𝑦 → ∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣))
 
Theoremax6e2ndeqVD 38167* The following User's Proof is a Virtual Deduction proof (see wvd1 37806) completed automatically by a Metamath tools program invoking mmj2 and the Metamath Proof Assistant. ax6e2eq 37794 is ax6e2ndeqVD 38167 without virtual deductions and was automatically derived from ax6e2ndeqVD 38167. (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: (∃𝑦¬ ∀𝑥𝑥 =