P. 439 of Theorem List - Metamath Proof Explorer

Type

Label

Description

Statement

Theorem

compne 43801

The complement of 𝐴 is not equal to 𝐴. (Contributed by Andrew Salmon, 15-Jul-2011.) (Proof shortened by BJ, 11-Nov-2021.)

⊢ (V ∖ 𝐴) ≠ 𝐴

Theorem

compab 43802

Two ways of saying "the complement of a class abstraction". (Contributed by Andrew Salmon, 15-Jul-2011.) (Proof shortened by Mario Carneiro, 11-Dec-2016.)

⊢ (V ∖ {𝑧 ∣ 𝜑}) = {𝑧 ∣ ¬ 𝜑}

Theorem

conss2 43803

Contrapositive law for subsets. (Contributed by Andrew Salmon, 15-Jul-2011.)

⊢ (𝐴 ⊆ (V ∖ 𝐵) ↔ 𝐵 ⊆ (V ∖ 𝐴))

Theorem

conss1 43804

Contrapositive law for subsets. (Contributed by Andrew Salmon, 15-Jul-2011.)

⊢ ((V ∖ 𝐴) ⊆ 𝐵 ↔ (V ∖ 𝐵) ⊆ 𝐴)

Theorem

ralbidar 43805

More general form of ralbida 3262. (Contributed by Andrew Salmon, 25-Jul-2011.)

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

Theorem

rexbidar 43806

More general form of rexbida 3264. (Contributed by Andrew Salmon, 25-Jul-2011.)

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

Theorem

dropab1 43807

Theorem to aid use of the distinctor reduction theorem with ordered pair class abstraction. (Contributed by Andrew Salmon, 25-Jul-2011.)

⊢ (∀𝑥 𝑥 = 𝑦 → {⟨𝑥, 𝑧⟩ ∣ 𝜑} = {⟨𝑦, 𝑧⟩ ∣ 𝜑})

Theorem

dropab2 43808

Theorem to aid use of the distinctor reduction theorem with ordered pair class abstraction. (Contributed by Andrew Salmon, 25-Jul-2011.)

⊢ (∀𝑥 𝑥 = 𝑦 → {⟨𝑧, 𝑥⟩ ∣ 𝜑} = {⟨𝑧, 𝑦⟩ ∣ 𝜑})

Theorem

ipo0 43809

If the identity relation partially orders any class, then that class is the null class. (Contributed by Andrew Salmon, 25-Jul-2011.)

⊢ ( I Po 𝐴 ↔ 𝐴 = ∅)

Theorem

ifr0 43810

A class that is founded by the identity relation is null. (Contributed by Andrew Salmon, 25-Jul-2011.)

⊢ ( I Fr 𝐴 ↔ 𝐴 = ∅)

Theorem

ordpss 43811

ordelpss 6391 with an antecedent removed. (Contributed by Andrew Salmon, 25-Jul-2011.)

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

Theorem

fvsb 43812*

Explicit substitution of a value of a function into a wff. (Contributed by Andrew Salmon, 1-Aug-2011.)

⊢ (∃!𝑦 𝐴𝐹𝑦 → ([(𝐹‘𝐴) / 𝑥]𝜑 ↔ ∃𝑥(∀𝑦(𝐴𝐹𝑦 ↔ 𝑦 = 𝑥) ∧ 𝜑)))

Theorem

fveqsb 43813*

Implicit substitution of a value of a function into a wff. (Contributed by Andrew Salmon, 1-Aug-2011.)

⊢ (𝑥 = (𝐹‘𝐴) → (𝜑 ↔ 𝜓))    &   ⊢ Ⅎ𝑥𝜓    ⇒   ⊢ (∃!𝑦 𝐴𝐹𝑦 → (𝜓 ↔ ∃𝑥(∀𝑦(𝐴𝐹𝑦 ↔ 𝑦 = 𝑥) ∧ 𝜑)))

Theorem

xpexb 43814

A Cartesian product exists iff its converse does. Corollary 6.9(1) in [TakeutiZaring] p. 26. (Contributed by Andrew Salmon, 13-Nov-2011.)

⊢ ((𝐴 × 𝐵) ∈ V ↔ (𝐵 × 𝐴) ∈ V)

Theorem

trelpss 43815

An element of a transitive set is a proper subset of it. Theorem 7.2 in [TakeutiZaring] p. 35. Unlike tz7.2 5656, ax-reg 9607 is required for its proof. (Contributed by Andrew Salmon, 13-Nov-2011.)

⊢ ((Tr 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ⊊ 𝐴)

21.38.6  Arithmetic

Theorem

addcomgi 43816

Generalization of commutative law for addition. Simplifies proofs dealing with vectors. However, it is dependent on our particular definition of ordered pair. (Contributed by Andrew Salmon, 28-Jan-2012.) (Revised by Mario Carneiro, 6-May-2015.)

⊢ (𝐴 + 𝐵) = (𝐵 + 𝐴)

21.38.7  Geometry

Syntax

cplusr 43817

Introduce the operation of vector addition.

class +_𝑟

Syntax

cminusr 43818

Introduce the operation of vector subtraction.

class -_𝑟

Syntax

ctimesr 43819

Introduce the operation of scalar multiplication.

class ._𝑣

Syntax

cptdfc 43820

PtDf is a predicate that is crucial for the definition of lines as well as proving a number of important theorems.

class PtDf(𝐴, 𝐵)

Syntax

crr3c 43821

RR3 is a class.

class RR3

Syntax

cline3 43822

line3 is a class.

class line3

Definition

df-addr 43823*

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

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

Definition

df-subr 43824*

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

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

Definition

df-mulv 43825*

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

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

Theorem

addrval 43826*

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

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

Theorem

subrval 43827*

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

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

Theorem

mulvval 43828*

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

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

Theorem

addrfv 43829

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 43830

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

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

Theorem

mulvfv 43831

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

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

Theorem

addrfn 43832

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

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

Theorem

subrfn 43833

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

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

Theorem

mulvfn 43834

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

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

Theorem

addrcom 43835

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

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

Definition

df-ptdf 43836*

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 43837

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

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.39  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 8398 in 2008.

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

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

Theorem

idiALT 43839

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 43840

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

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

Theorem

3impexpbicom 43841

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

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

Theorem

3impexpbicomi 43842

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

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

21.39.2  Supplementary unification deductions

Theorem

bi1imp 43843

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 43844

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

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

Theorem

bi3impb 43845

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

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

Theorem

bi3impa 43846

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

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

Theorem

bi23impib 43847

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

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

Theorem

bi13impib 43848

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

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

Theorem

bi123impib 43849

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

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

Theorem

bi13impia 43850

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

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

Theorem

bi123impia 43851

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

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

Theorem

bi33imp12 43852

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

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

Theorem

bi23imp13 43853

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

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

Theorem

bi13imp23 43854

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

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

Theorem

bi13imp2 43855

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

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

Theorem

bi12imp3 43856

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

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

Theorem

bi23imp1 43857

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

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

Theorem

bi123imp0 43858

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

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

Theorem

4animp1 43859

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 43860

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

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

Theorem

4an4132 43861

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

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

Theorem

expcomdg 43862

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

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

21.39.3  Conventional Metamath proofs, some derived from VD proofs

Theorem

iidn3 43863

idn3 43977 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 43864

e222 43998 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 43865

Right-biconditional form of e3 44099 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 43866

e13 44110 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 43867

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

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

Theorem

ee122 43868

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

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

Theorem

ee333 43869

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

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

Theorem

ee323 43870

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

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

Theorem

3ornot23 43871

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

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

Theorem

orbi1r 43872

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

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

Theorem

3orbi123 43873

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

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

Theorem

syl5imp 43874

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

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

Theorem

impexpd 43875

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 43876

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 43877

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 43878

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

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 43880

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 43881

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

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

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

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

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

Theorem

con5i 43885

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

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

Theorem

exlimexi 43886

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

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

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

Theorem

eexinst01 43888

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

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

Theorem

eexinst11 43889

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

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

Theorem

vk15.4j 43890

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

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

Theorem

notnotrALT 43891

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

⊢ (¬ ¬ 𝜑 → 𝜑)

Theorem

con3ALT2 43892

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

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

Theorem

ssralv2 43893*

Quantification restricted to a subclass for two quantifiers. ssralv 4046 for two quantifiers. The proof of ssralv2 43893 was automatically generated by minimizing the automatically translated proof of ssralv2VD 44228. 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 43894

sbcor 3827 with a 3-disjuncts. This proof is sbc3orgVD 44213 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 43895*

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

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

Theorem

rspsbc2 43896*

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

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

Theorem

sbcoreleleq 43897*

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

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

Theorem

tratrb 43898*

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

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

Theorem

ordelordALT 43899

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

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

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