P. 455 of Theorem List - Metamath Proof Explorer

Type

Label

Description

Statement

Definition

df-addr 45401*

Define the operation of vector addition. (Contributed by Andrew Salmon, 27-Jan-2012.)

⊢ +_𝑟 = (𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑣 ∈ ℝ ↦ ((𝑥‘𝑣) + (𝑦‘𝑣))))

Definition

df-subr 45402*

Define the operation of vector subtraction. (Contributed by Andrew Salmon, 27-Jan-2012.)

⊢ -_𝑟 = (𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑣 ∈ ℝ ↦ ((𝑥‘𝑣) − (𝑦‘𝑣))))

Definition

df-mulv 45403*

Define the operation of scalar multiplication. (Contributed by Andrew Salmon, 27-Jan-2012.)

⊢ ._𝑣 = (𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑣 ∈ ℝ ↦ (𝑥 · (𝑦‘𝑣))))

Theorem

addrval 45404*

Value of the operation of vector addition. (Contributed by Andrew Salmon, 27-Jan-2012.)

⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴+_𝑟𝐵) = (𝑣 ∈ ℝ ↦ ((𝐴‘𝑣) + (𝐵‘𝑣))))

Theorem

subrval 45405*

Value of the operation of vector subtraction. (Contributed by Andrew Salmon, 27-Jan-2012.)

⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴-_𝑟𝐵) = (𝑣 ∈ ℝ ↦ ((𝐴‘𝑣) − (𝐵‘𝑣))))

Theorem

mulvval 45406*

Value of the operation of scalar multiplication. (Contributed by Andrew Salmon, 27-Jan-2012.)

⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴._𝑣𝐵) = (𝑣 ∈ ℝ ↦ (𝐴 · (𝐵‘𝑣))))

Theorem

addrfv 45407

Vector addition at a value. The operation takes each vector 𝐴 and 𝐵 and forms a new vector whose values are the sum of each of the values of 𝐴 and 𝐵. (Contributed by Andrew Salmon, 27-Jan-2012.)

⊢ ((𝐴 ∈ 𝐸 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ ℝ) → ((𝐴+_𝑟𝐵)‘𝐶) = ((𝐴‘𝐶) + (𝐵‘𝐶)))

Theorem

subrfv 45408

Vector subtraction at a value. (Contributed by Andrew Salmon, 27-Jan-2012.)

⊢ ((𝐴 ∈ 𝐸 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ ℝ) → ((𝐴-_𝑟𝐵)‘𝐶) = ((𝐴‘𝐶) − (𝐵‘𝐶)))

Theorem

mulvfv 45409

Scalar multiplication at a value. (Contributed by Andrew Salmon, 27-Jan-2012.)

⊢ ((𝐴 ∈ 𝐸 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ ℝ) → ((𝐴._𝑣𝐵)‘𝐶) = (𝐴 · (𝐵‘𝐶)))

Theorem

addrfn 45410

Vector addition produces a function. (Contributed by Andrew Salmon, 27-Jan-2012.)

⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴+_𝑟𝐵) Fn ℝ)

Theorem

subrfn 45411

Vector subtraction produces a function. (Contributed by Andrew Salmon, 27-Jan-2012.)

⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴-_𝑟𝐵) Fn ℝ)

Theorem

mulvfn 45412

Scalar multiplication producees a function. (Contributed by Andrew Salmon, 27-Jan-2012.)

⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴._𝑣𝐵) Fn ℝ)

Theorem

addrcom 45413

Vector addition is commutative. (Contributed by Andrew Salmon, 28-Jan-2012.)

⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴+_𝑟𝐵) = (𝐵+_𝑟𝐴))

Definition

df-ptdf 45414*

Define the predicate PtDf, which is a utility definition used to shorten definitions and simplify proofs. (Contributed by Andrew Salmon, 15-Jul-2012.)

⊢ PtDf(𝐴, 𝐵) = (𝑥 ∈ ℝ ↦ (((𝑥._𝑣(𝐵-_𝑟𝐴)) +_𝑣 𝐴) “ {1, 2, 3}))

Definition

df-rr3 45415

Define the set of all points RR3. We define each point 𝐴 as a function to allow the use of vector addition and subtraction as well as scalar multiplication in our proofs. (Contributed by Andrew Salmon, 15-Jul-2012.)

⊢ RR3 = (ℝ ↑_m {1, 2, 3})

Definition

df-line3 45416*

Define the set of all lines. A line is an infinite subset of RR3 that satisfies a PtDf property. (Contributed by Andrew Salmon, 15-Jul-2012.)

⊢ line3 = {𝑥 ∈ 𝒫 RR3 ∣ (2_o ≼ 𝑥 ∧ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑧 ≠ 𝑦 → ran PtDf(𝑦, 𝑧) = 𝑥))}

21.43  Mathbox for Alan Sare

We are sad to report the passing of long-time contributor Alan Sare (Nov. 9, 1954 - Mar. 23, 2019).

Alan's first contribution to Metamath was a shorter proof for tfrlem8 8376 in 2008.

He developed a tool called "completeusersproof" that assists developing proofs using his "virtual deduction" method: https://us.metamath.org/other.html#completeusersproof 8376. His virtual deduction method is explained in the comment for wvd1 45508.

Below are some excerpts from his first emails to NM in 2007:

...I have been interested in proving set theory theorems for many years for mental exercise. I enjoy it. I have used a book by Martin Zuckerman. It is informal. I am interested in completely and perfectly proving theorems. Mr. Zuckerman leaves out most of the steps of a proof, of course, like most authors do, as you have noted. A complete proof for higher theorems would require a volume of writing similar to the Metamath documents. So I am frustrated when I am not capable of constructing a proof and Zuckerman leaves out steps I do not understand. I could search for the steps in other texts, but I don't do that too much. Metamath may be the answer for me....

...If we go beyond mathematics, I believe that it is possible to write down all human knowledge in a way similar to the way you have explicated large areas of mathematics. Of course, that would be a much, much more difficult job. For example, it is possible to take a hard science like physics, construct axioms based on experimental results, and to cast all of physics into a collection of axioms and theorems. Maybe this has already been attempted, although I am not familiar with it. When one then moves on to the soft sciences such as social science, this job gets much more difficult. The key is: All human thought consists of logical operations on abstract objects. Usually, these logical operations are done informally. There is no reason why one cannot take any subject and explicate it and take it down to the indivisible postulates in a formal rigorous way....

...When I read a math book or an engineering book I come across something I don't understand and I am compelled to understand it. But, often it is hopeless. I don't have the time. Or, I would have to read the same thing by multiple authors in the hope that different authors would give parts of the working proof that others have omitted. It is very inefficient. Because I have always been inclined to "get to the bottom" for a 100% fully understood proof....

21.43.1  Auxiliary theorems for the Virtual Deduction tool

Theorem

idiALT 45417

Placeholder for idi 1. Though unnecessary, this theorem is sometimes used in proofs in this mathbox for pedagogical purposes. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ 𝜑    ⇒   ⊢ 𝜑

Theorem

exbir 45418

Exportation implication also converting the consequent from a biconditional to an implication. Derived automatically from exbirVD 45791. (Contributed by Alan Sare, 31-Dec-2011.)

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

Theorem

3impexpbicom 45419

Version of 3impexp 1377 where in addition the consequent is commuted. (Contributed by Alan Sare, 31-Dec-2011.)

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

Theorem

3impexpbicomi 45420

Inference associated with 3impexpbicom 45419. Derived automatically from 3impexpbicomiVD 45796. (Contributed by Alan Sare, 31-Dec-2011.)

⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜏 ↔ 𝜃))))

21.43.2  Supplementary unification deductions

Theorem

bi1imp 45421

Importation inference similar to imp 412, except the outermost implication of the hypothesis is a biconditional. (Contributed by Alan Sare, 6-Nov-2017.)

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

Theorem

bi2imp 45422

Importation inference similar to imp 412, except both implications of the hypothesis are biconditionals. (Contributed by Alan Sare, 6-Nov-2017.)

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

Theorem

bi3impb 45423

Similar to 3impb 1132 with implication in hypothesis replaced by biconditional. (Contributed by Alan Sare, 6-Nov-2017.)

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

Theorem

bi3impa 45424

Similar to 3impa 1127 with implication in hypothesis replaced by biconditional. (Contributed by Alan Sare, 6-Nov-2017.)

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

Theorem

bi23impib 45425

3impib 1134 with the inner implication of the hypothesis a biconditional. (Contributed by Alan Sare, 6-Nov-2017.)

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

Theorem

bi13impib 45426

3impib 1134 with the outer implication of the hypothesis a biconditional. (Contributed by Alan Sare, 6-Nov-2017.)

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

Theorem

bi123impib 45427

3impib 1134 with the implications of the hypothesis biconditionals. (Contributed by Alan Sare, 6-Nov-2017.)

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

Theorem

bi13impia 45428

3impia 1135 with the outer implication of the hypothesis a biconditional. (Contributed by Alan Sare, 6-Nov-2017.)

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

Theorem

bi123impia 45429

3impia 1135 with the implications of the hypothesis biconditionals. (Contributed by Alan Sare, 6-Nov-2017.)

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

Theorem

bi33imp12 45430

3imp 1128 with innermost implication of the hypothesis a biconditional. (Contributed by Alan Sare, 6-Nov-2017.)

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

Theorem

bi13imp23 45431

3imp 1128 with outermost implication of the hypothesis a biconditional. (Contributed by Alan Sare, 6-Nov-2017.)

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

Theorem

bi13imp2 45432

Similar to 3imp 1128 except the outermost and innermost implications are biconditionals. (Contributed by Alan Sare, 6-Nov-2017.)

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

Theorem

bi12imp3 45433

Similar to 3imp 1128 except all but innermost implication are biconditionals. (Contributed by Alan Sare, 6-Nov-2017.)

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

Theorem

bi23imp1 45434

Similar to 3imp 1128 except all but outermost implication are biconditionals. (Contributed by Alan Sare, 6-Nov-2017.)

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

Theorem

bi123imp0 45435

Similar to 3imp 1128 except all implications are biconditionals. (Contributed by Alan Sare, 6-Nov-2017.)

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

Theorem

4animp1 45436

A single hypothesis unification deduction with an assertion which is an implication with a 4-right-nested conjunction antecedent. (Contributed by Alan Sare, 30-May-2018.)

⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜏 ↔ 𝜃))    ⇒   ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)

Theorem

4an31 45437

A rearrangement of conjuncts for a 4-right-nested conjunction. (Contributed by Alan Sare, 30-May-2018.)

⊢ ((((𝜒 ∧ 𝜓) ∧ 𝜑) ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)

Theorem

4an4132 45438

A rearrangement of conjuncts for a 4-right-nested conjunction. (Contributed by Alan Sare, 30-May-2018.)

⊢ ((((𝜃 ∧ 𝜒) ∧ 𝜓) ∧ 𝜑) → 𝜏)    ⇒   ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)

Theorem

expcomdg 45439

Biconditional form of expcomd 422. (Contributed by Alan Sare, 22-Jul-2012.) (New usage is discouraged.)

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

21.43.3  Conventional Metamath proofs, some derived from VD proofs

Theorem

iidn3 45440

idn3 45554 without virtual deduction connectives. Special theorem needed for the Virtual Deduction translation tool. (Contributed by Alan Sare, 23-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (𝜑 → (𝜓 → (𝜒 → 𝜒)))

Theorem

ee222 45441

e222 45575 without virtual deduction connectives. Special theorem needed for the Virtual Deduction translation tool. (Contributed by Alan Sare, 7-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → (𝜓 → 𝜃))    &   ⊢ (𝜑 → (𝜓 → 𝜏))    &   ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (𝜑 → (𝜓 → 𝜂))

Theorem

ee3bir 45442

Right-biconditional form of e3 45675 without virtual deduction connectives. Special theorem needed for the Virtual Deduction translation tool. (Contributed by Alan Sare, 22-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    &   ⊢ (𝜏 ↔ 𝜃)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜏)))

Theorem

ee13 45443

e13 45686 without virtual deduction connectives. Special theorem needed for the Virtual Deduction translation tool. (Contributed by Alan Sare, 28-Oct-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → (𝜒 → (𝜃 → 𝜏)))    &   ⊢ (𝜓 → (𝜏 → 𝜂))    ⇒   ⊢ (𝜑 → (𝜒 → (𝜃 → 𝜂)))

Theorem

ee121 45444

e121 45595 without virtual deductions. (Contributed by Alan Sare, 13-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → (𝜒 → 𝜃))    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜓 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (𝜑 → (𝜒 → 𝜂))

Theorem

ee122 45445

e122 45592 without virtual deductions. (Contributed by Alan Sare, 13-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → (𝜒 → 𝜃))    &   ⊢ (𝜑 → (𝜒 → 𝜏))    &   ⊢ (𝜓 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (𝜑 → (𝜒 → 𝜂))

Theorem

ee333 45446

e333 45671 without virtual deductions. (Contributed by Alan Sare, 17-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    &   ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜏)))    &   ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂)))    &   ⊢ (𝜃 → (𝜏 → (𝜂 → 𝜁)))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜁)))

Theorem

ee323 45447

e323 45704 without virtual deductions. (Contributed by Alan Sare, 17-Apr-2012.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    &   ⊢ (𝜑 → (𝜓 → 𝜏))    &   ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂)))    &   ⊢ (𝜃 → (𝜏 → (𝜂 → 𝜁)))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜁)))

Theorem

3ornot23 45448

If the second and third disjuncts of a true triple disjunction are false, then the first disjunct is true. Automatically derived from 3ornot23VD 45785. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → ((𝜒 ∨ 𝜑 ∨ 𝜓) → 𝜒))

Theorem

orbi1r 45449

orbi1 931 with order of disjuncts reversed. Derived from orbi1rVD 45786. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

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

Theorem

3orbi123 45450

pm4.39 992 with a 3-conjunct antecedent. This proof is 3orbi123VD 45788 automatically translated and minimized. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃) ∧ (𝜏 ↔ 𝜂)) → ((𝜑 ∨ 𝜒 ∨ 𝜏) ↔ (𝜓 ∨ 𝜃 ∨ 𝜂)))

Theorem

syl5imp 45451

Closed form of syl5 35. Derived automatically from syl5impVD 45801. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ ((𝜑 → (𝜓 → 𝜒)) → ((𝜃 → 𝜓) → (𝜑 → (𝜃 → 𝜒))))

Theorem

impexpd 45452

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. After the User's Proof was completed, it was minimized. The completed User's Proof before minimization is not shown. (Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.)

1::	⊢ (((𝜓 ∧ 𝜒) → 𝜃) ↔ (𝜓 → (𝜒 → 𝜃)))
qed:1:	⊢ ((𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) ↔ (𝜑 → (𝜓 → (𝜒 → 𝜃))))

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

Theorem

com3rgbi 45453

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. The completed Virtual Deduction Proof (not shown) was minimized. The minimized proof is shown. (Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.)

1::	⊢ ((𝜑 → (𝜓 → (𝜒 → 𝜃))) → (𝜑 → (𝜒 → (𝜓 → 𝜃))))
2::	⊢ ((𝜑 → (𝜒 → (𝜓 → 𝜃))) → (𝜒 → (𝜑 → (𝜓 → 𝜃))))
3:1,2:	⊢ ((𝜑 → (𝜓 → (𝜒 → 𝜃))) → (𝜒 → (𝜑 → (𝜓 → 𝜃))))
4::	⊢ ((𝜒 → (𝜑 → (𝜓 → 𝜃))) → (𝜑 → (𝜒 → (𝜓 → 𝜃))))
5::	⊢ ((𝜑 → (𝜒 → (𝜓 → 𝜃))) → (𝜑 → (𝜓 → (𝜒 → 𝜃))))
6:4,5:	⊢ ((𝜒 → (𝜑 → (𝜓 → 𝜃))) → (𝜑 → (𝜓 → (𝜒 → 𝜃))))
qed:3,6:	⊢ ((𝜑 → (𝜓 → (𝜒 → 𝜃))) ↔ (𝜒 → (𝜑 → (𝜓 → 𝜃))))

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

Theorem

impexpdcom 45454

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. The completed Virtual Deduction Proof (not shown) was minimized. The minimized proof is shown. (Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.)

1::	⊢ ((𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) ↔ (𝜑 → (𝜓 → (𝜒 → 𝜃))))
2::	⊢ ((𝜓 → (𝜒 → (𝜑 → 𝜃))) ↔ (𝜑 → (𝜓 → (𝜒 → 𝜃))))
qed:1,2:	⊢ ((𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) ↔ (𝜓 → (𝜒 → (𝜑 → 𝜃))))

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

Theorem

ee1111 45455

Non-virtual deduction form of e1111 45614. (Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.) 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. The completed Virtual Deduction Proof (not shown) was minimized. The minimized proof is shown.

h1::	⊢ (𝜑 → 𝜓)
h2::	⊢ (𝜑 → 𝜒)
h3::	⊢ (𝜑 → 𝜃)
h4::	⊢ (𝜑 → 𝜏)
h5::	⊢ (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂))))
6:1,5:	⊢ (𝜑 → (𝜒 → (𝜃 → (𝜏 → 𝜂))))
7:6:	⊢ (𝜒 → (𝜑 → (𝜃 → (𝜏 → 𝜂))))
8:2,7:	⊢ (𝜑 → (𝜑 → (𝜃 → (𝜏 → 𝜂))))
9:8:	⊢ (𝜑 → (𝜃 → (𝜏 → 𝜂)))
10:9:	⊢ (𝜃 → (𝜑 → (𝜏 → 𝜂)))
11:3,10:	⊢ (𝜑 → (𝜑 → (𝜏 → 𝜂)))
12:11:	⊢ (𝜑 → (𝜏 → 𝜂))
13:12:	⊢ (𝜏 → (𝜑 → 𝜂))
14:4,13:	⊢ (𝜑 → (𝜑 → 𝜂))
qed:14:	⊢ (𝜑 → 𝜂)

⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂))))    ⇒   ⊢ (𝜑 → 𝜂)

Theorem

pm2.43bgbi 45456

Logical equivalence of a 2-left-nested implication and a 1-left-nested implicated when two antecedents of the former implication are identical. (Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.) 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. The completed Virtual Deduction Proof (not shown) was minimized. The minimized proof is shown.

1::	⊢ ((𝜑 → (𝜓 → (𝜑 → 𝜒))) → (𝜑 → (𝜑 → (𝜓 → 𝜒))))
2::	⊢ ((𝜑 → (𝜑 → (𝜓 → 𝜒))) → (𝜑 → (𝜓 → 𝜒)))
3:1,2:	⊢ ((𝜑 → (𝜓 → (𝜑 → 𝜒))) → (𝜑 → (𝜓 → 𝜒)))
4::	⊢ ((𝜑 → (𝜓 → 𝜒)) → (𝜓 → (𝜑 → 𝜒)))
5:3,4:	⊢ ((𝜑 → (𝜓 → (𝜑 → 𝜒))) → (𝜓 → (𝜑 → 𝜒)))
6::	⊢ ((𝜓 → (𝜑 → 𝜒)) → (𝜑 → (𝜓 → (𝜑 → 𝜒))))
qed:5,6:	⊢ ((𝜑 → (𝜓 → (𝜑 → 𝜒))) ↔ (𝜓 → (𝜑 → 𝜒)))

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

Theorem

pm2.43cbi 45457

Logical equivalence of a 3-left-nested implication and a 2-left-nested implicated when two antecedents of the former implication are identical. (Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.) 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. The completed Virtual Deduction Proof (not shown) was minimized. The minimized proof is shown.

1::	⊢ ((𝜑 → (𝜓 → (𝜒 → (𝜑 → 𝜃))) ) → (𝜑 → (𝜓 → (𝜑 → (𝜒 → 𝜃)))))
2::	⊢ ((𝜑 → (𝜓 → (𝜑 → (𝜒 → 𝜃))) ) → (𝜓 → (𝜑 → (𝜒 → 𝜃))))
3:1,2:	⊢ ((𝜑 → (𝜓 → (𝜒 → (𝜑 → 𝜃))) ) → (𝜓 → (𝜑 → (𝜒 → 𝜃))))
4::	⊢ ((𝜓 → (𝜑 → (𝜒 → 𝜃))) → (𝜓 → (𝜒 → (𝜑 → 𝜃))))
5:3,4:	⊢ ((𝜑 → (𝜓 → (𝜒 → (𝜑 → 𝜃))) ) → (𝜓 → (𝜒 → (𝜑 → 𝜃))))
6::	⊢ ((𝜓 → (𝜒 → (𝜑 → 𝜃))) → (𝜑 → (𝜓 → (𝜒 → (𝜑 → 𝜃)))))
qed:5,6:	⊢ ((𝜑 → (𝜓 → (𝜒 → (𝜑 → 𝜃))) ) ↔ (𝜓 → (𝜒 → (𝜑 → 𝜃))))

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

Theorem

ee233 45458

Non-virtual deduction form of e233 45703. (Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.) 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. The completed Virtual Deduction Proof (not shown) was minimized. The minimized proof is shown.

h1::	⊢ (𝜑 → (𝜓 → 𝜒))
h2::	⊢ (𝜑 → (𝜓 → (𝜃 → 𝜏)))
h3::	⊢ (𝜑 → (𝜓 → (𝜃 → 𝜂)))
h4::	⊢ (𝜒 → (𝜏 → (𝜂 → 𝜁)))
5:1,4:	⊢ (𝜑 → (𝜓 → (𝜏 → (𝜂 → 𝜁))) )
6:5:	⊢ (𝜏 → (𝜑 → (𝜓 → (𝜂 → 𝜁))) )
7:2,6:	⊢ (𝜑 → (𝜓 → (𝜃 → (𝜑 → (𝜓 → (𝜂 → 𝜁))))))
8:7:	⊢ (𝜓 → (𝜃 → (𝜑 → (𝜓 → (𝜂 → 𝜁)))))
9:8:	⊢ (𝜃 → (𝜑 → (𝜓 → (𝜂 → 𝜁))) )
10:9:	⊢ (𝜑 → (𝜓 → (𝜃 → (𝜂 → 𝜁))) )
11:10:	⊢ (𝜂 → (𝜑 → (𝜓 → (𝜃 → 𝜁))) )
12:3,11:	⊢ (𝜑 → (𝜓 → (𝜃 → (𝜑 → (𝜓 → (𝜃 → 𝜁))))))
13:12:	⊢ (𝜓 → (𝜃 → (𝜑 → (𝜓 → (𝜃 → 𝜁)))))
14:13:	⊢ (𝜃 → (𝜑 → (𝜓 → (𝜃 → 𝜁))) )
qed:14:	⊢ (𝜑 → (𝜓 → (𝜃 → 𝜁)))

⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜏)))    &   ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜂)))    &   ⊢ (𝜒 → (𝜏 → (𝜂 → 𝜁)))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜁)))

Theorem

imbi13 45459

Join three logical equivalences to form equivalence of implications. imbi13 45459 is imbi13VD 45812 without virtual deductions and was automatically derived from imbi13VD 45812 using the tools program translate..without..overwriting.cmd and Metamath's minimize command. (Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ ((𝜑 ↔ 𝜓) → ((𝜒 ↔ 𝜃) → ((𝜏 ↔ 𝜂) → ((𝜑 → (𝜒 → 𝜏)) ↔ (𝜓 → (𝜃 → 𝜂))))))

Theorem

ee33 45460

Non-virtual deduction form of e33 45672. (Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.) 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. The completed Virtual Deduction Proof (not shown) was minimized. The minimized proof is shown.

h1::	⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
h2::	⊢ (𝜑 → (𝜓 → (𝜒 → 𝜏)))
h3::	⊢ (𝜃 → (𝜏 → 𝜂))
4:1,3:	⊢ (𝜑 → (𝜓 → (𝜒 → (𝜏 → 𝜂))))
5:4:	⊢ (𝜏 → (𝜑 → (𝜓 → (𝜒 → 𝜂))))
6:2,5:	⊢ (𝜑 → (𝜓 → (𝜒 → (𝜑 → (𝜓 → (𝜒 → 𝜂))))))
7:6:	⊢ (𝜓 → (𝜒 → (𝜑 → (𝜓 → (𝜒 → 𝜂)))))
8:7:	⊢ (𝜒 → (𝜑 → (𝜓 → (𝜒 → 𝜂))))
qed:8:	⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂)))

⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    &   ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜏)))    &   ⊢ (𝜃 → (𝜏 → 𝜂))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂)))

Theorem

con5 45461

Biconditional contraposition variation. This proof is con5VD 45838 automatically translated and minimized. (Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.)

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

Theorem

con5i 45462

Inference form of con5 45461. (Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.)

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

Theorem

exlimexi 45463

Inference similar to Theorem 19.23 of [Margaris] p. 90. (Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (𝜓 → ∀𝑥𝜓)    &   ⊢ (∃𝑥𝜑 → (𝜑 → 𝜓))    ⇒   ⊢ (∃𝑥𝜑 → 𝜓)

Theorem

sb5ALT 45464*

Equivalence for substitution. Alternate proof of sb5 2310. This proof is sb5ALTVD 45851 automatically translated and minimized. (Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.)

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

Theorem

eexinst01 45465

exinst01 45564 without virtual deductions. (Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ ∃𝑥𝜓    &   ⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜒 → ∀𝑥𝜒)    ⇒   ⊢ (𝜑 → 𝜒)

Theorem

eexinst11 45466

exinst11 45565 without virtual deductions. (Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (𝜑 → ∃𝑥𝜓)    &   ⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜒 → ∀𝑥𝜒)    ⇒   ⊢ (𝜑 → 𝜒)

Theorem

vk15.4j 45467

Excercise 4j of Unit 15 of "Understanding Symbolic Logic", Fifth Edition (2008), by Virginia Klenk. This proof is the minimized Hilbert-style axiomatic version of the Fitch-style Natural Deduction proof found on page 442 of Klenk and was automatically derived from that proof. vk15.4j 45467 is vk15.4jVD 45852 automatically translated and minimized. (Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.)

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

Theorem

notnotrALT 45468

Converse of double negation. Alternate proof of notnotr 131. This proof is notnotrALTVD 45853 automatically translated and minimized. (Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (¬ ¬ 𝜑 → 𝜑)

Theorem

con3ALT2 45469

Contraposition. Alternate proof of con3 154. This proof is con3ALTVD 45854 automatically translated and minimized. (Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.)

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

Theorem

ssralv2 45470*

Quantification restricted to a subclass for two quantifiers. ssralv 4000 for two quantifiers. The proof of ssralv2 45470 was automatically generated by minimizing the automatically translated proof of ssralv2VD 45804. The automatic translation is by the tools program translate_without_overwriting.cmd. (Contributed by Alan Sare, 18-Feb-2012.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷 𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐶 𝜑))

Theorem

sbc3or 45471

sbcor 3789 with a 3-disjuncts. This proof is sbc3orgVD 45789 automatically translated and minimized. (Contributed by Alan Sare, 31-Dec-2011.) (Revised by NM, 24-Aug-2018.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ ([𝐴 / 𝑥](𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ([𝐴 / 𝑥]𝜑 ∨ [𝐴 / 𝑥]𝜓 ∨ [𝐴 / 𝑥]𝜒))

Theorem

alrim3con13v 45472*

Closed form of alrimi 2250 with 2 additional conjuncts having no occurrences of the quantifying variable. This proof is 19.21a3con13vVD 45790 automatically translated and minimized. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

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

Theorem

rspsbc2 45473*

rspsbc 3826 with two quantifying variables. This proof is rspsbc2VD 45793 automatically translated and minimized. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (𝐴 ∈ 𝐵 → (𝐶 ∈ 𝐷 → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷 𝜑 → [𝐶 / 𝑦][𝐴 / 𝑥]𝜑)))

Theorem

sbcoreleleq 45474*

Substitution of a setvar variable for another setvar variable in a 3-conjunct formula. Derived automatically from sbcoreleleqVD 45797. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑦](𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ↔ (𝑥 ∈ 𝐴 ∨ 𝐴 ∈ 𝑥 ∨ 𝑥 = 𝐴)))

Theorem

tratrb 45475*

If a class is transitive and any two distinct elements of the class are E-comparable, then every element of that class is transitive. Derived automatically from tratrbVD 45799. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ ((Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴) → Tr 𝐵)

Theorem

ordelordALT 45476

An element of an ordinal class is ordinal. Proposition 7.6 of [TakeutiZaring] p. 36. This is an alternate proof of ordelord 6377 using the Axiom of Regularity indirectly through dford2 9605. 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. ordelordALT 45476 is ordelordALTVD 45805 without virtual deductions and was automatically derived from ordelordALTVD 45805 using the tools program translate..without..overwriting.cmd and Metamath's minimize command. (Contributed by Alan Sare, 18-Feb-2012.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → Ord 𝐵)

Theorem

sbcim2g 45477

Distribution of class substitution over a left-nested implication. Similar to sbcimg 3787. sbcim2g 45477 is sbcim2gVD 45813 without virtual deductions and was automatically derived from sbcim2gVD 45813 using the tools program translate..without..overwriting.cmd and Metamath's minimize command. (Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥](𝜑 → (𝜓 → 𝜒)) ↔ ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒))))

Theorem

sbcbi 45478

Implication form of sbcbii 3795. sbcbi 45478 is sbcbiVD 45814 without virtual deductions and was automatically derived from sbcbiVD 45814 using the tools program translate..without..overwriting.cmd and Metamath's minimize command. (Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝜑 ↔ 𝜓) → ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓)))

Theorem

trsbc 45479*

Formula-building inference rule for class substitution, substituting a class variable for the setvar variable of the transitivity predicate. trsbc 45479 is trsbcVD 45815 without virtual deductions and was automatically derived from trsbcVD 45815 using the tools program translate..without..overwriting.cmd and Metamath's minimize command. (Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]Tr 𝑥 ↔ Tr 𝐴))

Theorem

truniALT 45480*

The union of a class of transitive sets is transitive. Alternate proof of truni 5228. truniALT 45480 is truniALTVD 45816 without virtual deductions and was automatically derived from truniALTVD 45816 using the tools program translate..without..overwriting.cmd and Metamath's minimize command. (Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (∀𝑥 ∈ 𝐴 Tr 𝑥 → Tr ∪ 𝐴)

Theorem

onfrALTlem5 45481*

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

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

Theorem

onfrALTlem4 45482*

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

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

Theorem

onfrALTlem3 45483*

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

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

Theorem

ggen31 45484*

gen31 45560 without virtual deductions. (Contributed by Alan Sare, 22-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → ∀𝑥𝜃)))

Theorem

onfrALTlem2 45485*

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

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

Theorem

cbvexsv 45486*

A theorem pertaining to the substitution for an existentially quantified variable when the substituted variable does not occur in the quantified wff. (Contributed by Alan Sare, 22-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (∃𝑥𝜑 ↔ ∃𝑦[𝑦 / 𝑥]𝜑)

Theorem

onfrALTlem1 45487*

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

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

Theorem

onfrALT 45488

The membership relation is foundational on the class of ordinal numbers. onfrALT 45488 is an alternate proof of onfr 6395. onfrALTVD 45829 is the Virtual Deduction proof from which onfrALT 45488 is derived. The Virtual Deduction proof mirrors the working proof of onfr 6395 which is the main part of the proof of Theorem 7.12 of the first edition of TakeutiZaring. The proof of the corresponding Proposition 7.12 of [TakeutiZaring] p. 38 (second edition) does not contain the working proof equivalent of onfrALTVD 45829. This theorem does not rely on the Axiom of Regularity. (Contributed by Alan Sare, 22-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ E Fr On

Theorem

19.41rg 45489

Closed form of right-to-left implication of 19.41 2272, Theorem 19.41 of [Margaris] p. 90. Derived from 19.41rgVD 45840. (Contributed by Alan Sare, 8-Feb-2014.) (Proof modification is discouraged.) (New usage is discouraged.)

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

Theorem

opelopab4 45490*

Ordered pair membership in a class abstraction of ordered pairs. Compare to elopab 5501. (Contributed by Alan Sare, 8-Feb-2014.) (Revised by Mario Carneiro, 6-May-2015.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (⟨𝑢, 𝑣⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑))

Theorem

2pm13.193 45491

pm13.193 45351 for two variables. pm13.193 45351 is Theorem *13.193 in [WhiteheadRussell] p. 179. Derived from 2pm13.193VD 45841. (Contributed by Alan Sare, 8-Feb-2014.) (Proof modification is discouraged.) (New usage is discouraged.)

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

Theorem

hbntal 45492

A closed form of hbn 2329. hbnt 2328 is another closed form of hbn 2329. (Contributed by Alan Sare, 8-Feb-2014.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (∀𝑥(𝜑 → ∀𝑥𝜑) → ∀𝑥(¬ 𝜑 → ∀𝑥 ¬ 𝜑))

Theorem

hbimpg 45493

A closed form of hbim 2333. Derived from hbimpgVD 45842. (Contributed by Alan Sare, 8-Feb-2014.) (Proof modification is discouraged.) (New usage is discouraged.)

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

Theorem

hbalg 45494

Closed form of hbal 2204. Derived from hbalgVD 45843. (Contributed by Alan Sare, 8-Feb-2014.) (Proof modification is discouraged.) (New usage is discouraged.)

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

Theorem

hbexg 45495

Closed form of nfex 2355. Derived from hbexgVD 45844. (Contributed by Alan Sare, 8-Feb-2014.) (Revised by Mario Carneiro, 12-Dec-2016.) (Proof modification is discouraged.) (New usage is discouraged.)

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

Theorem

ax6e2eq 45496*

Alternate form of ax6e 2413 for non-distinct 𝑥, 𝑦 and 𝑢 = 𝑣. ax6e2eq 45496 is derived from ax6e2eqVD 45845. (Contributed by Alan Sare, 25-Mar-2014.) (Proof modification is discouraged.) (New usage is discouraged.)

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

Theorem

ax6e2nd 45497*

If at least two sets exist (dtru 5405), then the same is true expressed in an alternate form similar to the form of ax6e 2413. ax6e2nd 45497 is derived from ax6e2ndVD 45846. (Contributed by Alan Sare, 25-Mar-2014.) (Proof modification is discouraged.) (New usage is discouraged.)

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

Theorem

ax6e2ndeq 45498*

"At least two sets exist" expressed in the form of dtru 5405 is logically equivalent to the same expressed in a form similar to ax6e 2413 if dtru 5405 is false implies 𝑢 = 𝑣. ax6e2ndeq 45498 is derived from ax6e2ndeqVD 45847. (Contributed by Alan Sare, 25-Mar-2014.) (Proof modification is discouraged.) (New usage is discouraged.)

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

Theorem

2sb5nd 45499*

Equivalence for double substitution 2sb5 2312 without distinct 𝑥, 𝑦 requirement. 2sb5nd 45499 is derived from 2sb5ndVD 45848. (Contributed by Alan Sare, 30-Apr-2014.) (Proof modification is discouraged.) (New usage is discouraged.)

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

Theorem

2uasbanh 45500*

Distribute the unabbreviated form of proper substitution in and out of a conjunction. 2uasbanh 45500 is derived from 2uasbanhVD 45849. (Contributed by Alan Sare, 31-May-2014.) (Proof modification is discouraged.) (New usage is discouraged.)

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