P. 448 of Theorem List - Metamath Proof Explorer

Type

Label

Description

Statement

Definition

df-mulv 44701*

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

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

Theorem

addrval 44702*

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

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

Theorem

subrval 44703*

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

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

Theorem

mulvval 44704*

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

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

Theorem

addrfv 44705

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 44706

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

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

Theorem

mulvfv 44707

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

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

Theorem

addrfn 44708

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

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

Theorem

subrfn 44709

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

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

Theorem

mulvfn 44710

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

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

Theorem

addrcom 44711

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

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

Definition

df-ptdf 44712*

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 44713

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

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.41  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 8315 in 2008.

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

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.41.1  Auxiliary theorems for the Virtual Deduction tool

Theorem

idiALT 44715

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 44716

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

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

Theorem

3impexpbicom 44717

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

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

Theorem

3impexpbicomi 44718

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

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

21.41.2  Supplementary unification deductions

Theorem

bi1imp 44719

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

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

Theorem

bi2imp 44720

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

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

Theorem

bi3impb 44721

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

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

Theorem

bi3impa 44722

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

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

Theorem

bi23impib 44723

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

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

Theorem

bi13impib 44724

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

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

Theorem

bi123impib 44725

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

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

Theorem

bi13impia 44726

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

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

Theorem

bi123impia 44727

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

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

Theorem

bi33imp12 44728

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

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

Theorem

bi13imp23 44729

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

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

Theorem

bi13imp2 44730

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

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

Theorem

bi12imp3 44731

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

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

Theorem

bi23imp1 44732

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

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

Theorem

bi123imp0 44733

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

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

Theorem

4animp1 44734

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 44735

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

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

Theorem

4an4132 44736

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

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

Theorem

expcomdg 44737

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

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

21.41.3  Conventional Metamath proofs, some derived from VD proofs

Theorem

iidn3 44738

idn3 44852 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 44739

e222 44873 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 44740

Right-biconditional form of e3 44973 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 44741

e13 44984 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 44742

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

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

Theorem

ee122 44743

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

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

Theorem

ee333 44744

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

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

Theorem

ee323 44745

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

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

Theorem

3ornot23 44746

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

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

Theorem

orbi1r 44747

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

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

Theorem

3orbi123 44748

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

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

Theorem

syl5imp 44749

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

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

Theorem

impexpd 44750

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 44751

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 44752

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 44753

Non-virtual deduction form of e1111 44912. (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 44754

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 44755

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 44756

Non-virtual deduction form of e233 45001. (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 44757

Join three logical equivalences to form equivalence of implications. imbi13 44757 is imbi13VD 45110 without virtual deductions and was automatically derived from imbi13VD 45110 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 44758

Non-virtual deduction form of e33 44970. (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 44759

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

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

Theorem

con5i 44760

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

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

Theorem

exlimexi 44761

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

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

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

Theorem

eexinst01 44763

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

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

Theorem

eexinst11 44764

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

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

Theorem

vk15.4j 44765

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 44765 is vk15.4jVD 45150 automatically translated and minimized. (Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.)

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

Theorem

notnotrALT 44766

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

⊢ (¬ ¬ 𝜑 → 𝜑)

Theorem

con3ALT2 44767

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

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

Theorem

ssralv2 44768*

Quantification restricted to a subclass for two quantifiers. ssralv 4002 for two quantifiers. The proof of ssralv2 44768 was automatically generated by minimizing the automatically translated proof of ssralv2VD 45102. 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 44769

sbcor 3791 with a 3-disjuncts. This proof is sbc3orgVD 45087 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 44770*

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

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

Theorem

rspsbc2 44771*

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

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

Theorem

sbcoreleleq 44772*

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

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

Theorem

tratrb 44773*

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 45097. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

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

Theorem

ordelordALT 44774

An element of an ordinal class is ordinal. Proposition 7.6 of [TakeutiZaring] p. 36. This is an alternate proof of ordelord 6339 using the Axiom of Regularity indirectly through dford2 9529. 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 44774 is ordelordALTVD 45103 without virtual deductions and was automatically derived from ordelordALTVD 45103 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 44775

Distribution of class substitution over a left-nested implication. Similar to sbcimg 3789. sbcim2g 44775 is sbcim2gVD 45111 without virtual deductions and was automatically derived from sbcim2gVD 45111 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 44776

Implication form of sbcbii 3797. sbcbi 44776 is sbcbiVD 45112 without virtual deductions and was automatically derived from sbcbiVD 45112 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 44777*

Formula-building inference rule for class substitution, substituting a class variable for the setvar variable of the transitivity predicate. trsbc 44777 is trsbcVD 45113 without virtual deductions and was automatically derived from trsbcVD 45113 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 44778*

The union of a class of transitive sets is transitive. Alternate proof of truni 5220. truniALT 44778 is truniALTVD 45114 without virtual deductions and was automatically derived from truniALTVD 45114 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 44779*

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

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

Theorem

onfrALTlem4 44780*

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

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

Theorem

onfrALTlem3 44781*

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

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

Theorem

ggen31 44782*

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

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

Theorem

onfrALTlem2 44783*

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

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

Theorem

cbvexsv 44784*

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

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

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

Theorem

onfrALT 44786

The membership relation is foundational on the class of ordinal numbers. onfrALT 44786 is an alternate proof of onfr 6356. onfrALTVD 45127 is the Virtual Deduction proof from which onfrALT 44786 is derived. The Virtual Deduction proof mirrors the working proof of onfr 6356 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 45127. 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 44787

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

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

Theorem

opelopab4 44788*

Ordered pair membership in a class abstraction of ordered pairs. Compare to elopab 5475. (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 44789

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

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

Theorem

hbntal 44790

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

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

Theorem

hbimpg 44791

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

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

Theorem

hbalg 44792

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

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

Theorem

hbexg 44793

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

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

Theorem

ax6e2eq 44794*

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

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

Theorem

ax6e2nd 44795*

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

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

Theorem

ax6e2ndeq 44796*

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

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

Theorem

2sb5nd 44797*

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

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

Theorem

2uasbanh 44798*

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

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

Theorem

2uasban 44799*

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

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

Theorem

e2ebind 44800

Absorption of an existential quantifier of a double existential quantifier of non-distinct variables. e2ebind 44800 is derived from e2ebindVD 45148. (Contributed by Alan Sare, 27-Nov-2014.) (Proof modification is discouraged.) (New usage is discouraged.)

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