Metamath Proof Explorer - mmtheorems8

Jump to page: 1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5787

Statement List for Metamath Proof Explorer - 701-800 - Page 8 of 58

Type	Label	Description
Statement
Theorem	hbex 701	If x is not free in φ, it is not free in ∃yφ.
⊢ (φ → ∀xφ)    ⇒   ⊢ (∃yφ → ∀x∃yφ)
Theorem	hbim 702	If x is not free in φ and ψ, it is not free in (φ → ψ).
⊢ (φ → ∀xφ)    &   ⊢ (ψ → ∀xψ)    ⇒   ⊢ ((φ → ψ) → ∀x(φ → ψ))
Theorem	hbor 703	If x is not free in φ and ψ, it is not free in (φ ∨ ψ).
⊢ (φ → ∀xφ)    &   ⊢ (ψ → ∀xψ)    ⇒   ⊢ ((φ ∨ ψ) → ∀x(φ ∨ ψ))
Theorem	hban 704	If x is not free in φ and ψ, it is not free in (φ ∧ ψ).
⊢ (φ → ∀xφ)    &   ⊢ (ψ → ∀xψ)    ⇒   ⊢ ((φ ∧ ψ) → ∀x(φ ∧ ψ))
Theorem	hbbi 705	If x is not free in φ and ψ, it is not free in (φ ↔ ψ).
⊢ (φ → ∀xφ)    &   ⊢ (ψ → ∀xψ)    ⇒   ⊢ ((φ ↔ ψ) → ∀x(φ ↔ ψ))
Theorem	hb3or 706	If x is not free in φ, ψ, and χ, it is not free in (φ ∨ ψ ∨ χ).
⊢ (φ → ∀xφ)    &   ⊢ (ψ → ∀xψ)    &   ⊢ (χ → ∀xχ)    ⇒   ⊢ ((φ ∨ ψ ∨ χ) → ∀x(φ ∨ ψ ∨ χ))
Theorem	hb3an 707	If x is not free in φ, ψ, and χ, it is not free in (φ ∧ ψ ∧ χ).
⊢ (φ → ∀xφ)    &   ⊢ (ψ → ∀xψ)    &   ⊢ (χ → ∀xχ)    ⇒   ⊢ ((φ ∧ ψ ∧ χ) → ∀x(φ ∧ ψ ∧ χ))
Theorem	hbn1 708	x is not free in ¬ ∀xφ.
⊢ (¬ ∀xφ → ∀x ¬ ∀xφ)
Theorem	hbe1 709	x is not free in ∃xφ.
⊢ (∃xφ → ∀x∃xφ)
Theorem	hbnt 710	A closed form of hypothesis builder hbne 699.
⊢ (∀x(φ → ∀xφ) → (¬ φ → ∀x ¬ φ))
Theorem	ax6 711	Axiom C5-2 of [Monk2] p. 113, which we prove from our ax-6 675 (and others). Conversely, ax-6 675 follows from this using ax-4 673 and propositional calculus, showing that they are interchangeable.
⊢ (¬ ∀xφ → ∀x ¬ ∀xφ)
Theorem	19.8a 712	If a wff is true, it is true for at least one instance.
⊢ (φ → ∃xφ)
Theorem	19.2 713	Theorem 19.2 of [Margaris] p. 89.
⊢ (∀xφ → ∃xφ)
Theorem	19.3r 714	A wff may be quantified with a variable not free in it.
⊢ (φ → ∀xφ)    ⇒   ⊢ (φ ↔ ∀xφ)
Theorem	alcom 715	Theorem 19.5 of [Margaris] p. 89.
⊢ (∀x∀yφ ↔ ∀y∀xφ)
Theorem	alnex 716	Theorem 19.7 of [Margaris] p. 89.
⊢ (∀x ¬ φ ↔ ¬ ∃xφ)
Theorem	alex 717	Theorem 19.6 of [Margaris] p. 89.
⊢ (∀xφ ↔ ¬ ∃x ¬ φ)
Theorem	19.9r 718	Variation of Theorem 19.9 of [Margaris] p. 89.
⊢ (φ → ∀xφ)    ⇒   ⊢ (φ ↔ ∃xφ)
Theorem	19.9t 719	A closed version of one direction of 19.9r 718.
⊢ (∀x(φ → ∀xφ) → (∃xφ → φ))
Theorem	19.9d 720	A deduction version of one direction of 19.9r 718.
⊢ (ψ → ∀xψ)    &   ⊢ (ψ → (φ → ∀xφ))    ⇒   ⊢ (ψ → (∃xφ → φ))
Theorem	exnal 721	Theorem 19.14 of [Margaris] p. 90.
⊢ (∃x ¬ φ ↔ ¬ ∀xφ)
Theorem	19.22 722	Theorem 19.22 of [Margaris] p. 90.
⊢ (∀x(φ → ψ) → (∃xφ → ∃xψ))
Theorem	19.22i 723	Inference adding existential quantifier to antecedent and consequent.
⊢ (φ → ψ)    ⇒   ⊢ (∃xφ → ∃xψ)
Theorem	alinexa 724	A transformation of quantifiers and logical connectives.
⊢ (∀x(φ → ¬ ψ) ↔ ¬ ∃x(φ ∧ ψ))
Theorem	exanali 725	A transformation of quantifiers and logical connectives.
⊢ (∃x(φ ∧ ¬ ψ) ↔ ¬ ∀x(φ → ψ))
Theorem	alexn 726	A relationship between two quantifiers and negation.
⊢ (∀x∃y ¬ φ ↔ ¬ ∃x∀yφ)
Theorem	excomim 727	One direction of Theorem 19.11 of [Margaris] p. 89.
⊢ (∃x∃yφ → ∃y∃xφ)
Theorem	excom 728	Theorem 19.11 of [Margaris] p. 89.
⊢ (∃x∃yφ ↔ ∃y∃xφ)
Theorem	19.12 729	Theorem 19.12 of [Margaris] p. 89. Assuming the converse is a mistake sometimes made by beginners! But sometimes the converse does hold, as in 19.12vv 960.
⊢ (∃x∀yφ → ∀y∃xφ)
Theorem	19.16 730	Theorem 19.16 of [Margaris] p. 90.
⊢ (φ → ∀xφ)    ⇒   ⊢ (∀x(φ ↔ ψ) → (φ ↔ ∀xψ))
Theorem	19.17 731	Theorem 19.17 of [Margaris] p. 90.
⊢ (ψ → ∀xψ)    ⇒   ⊢ (∀x(φ ↔ ψ) → (∀xφ ↔ ψ))
Theorem	19.18 732	Theorem 19.18 of [Margaris] p. 90.
⊢ (∀x(φ ↔ ψ) → (∃xφ ↔ ∃xψ))
Theorem	biex 733	Inference adding existential quantifier to both sides of an equivalence.
⊢ (φ ↔ ψ)    ⇒   ⊢ (∃xφ ↔ ∃xψ)
Theorem	bi2ex 734	Inference adding 2 existential quantifiers to both sides of an equivalence.
⊢ (φ ↔ ψ)    ⇒   ⊢ (∃x∃yφ ↔ ∃x∃yψ)
Theorem	bi3ex 735	Inference adding 3 existential quantifiers to both sides of an equivalence.
⊢ (φ ↔ ψ)    ⇒   ⊢ (∃x∃y∃zφ ↔ ∃x∃y∃zψ)
Theorem	exancom 736	Commutation of conjunction inside an existential quantifier.
⊢ (∃x(φ ∧ ψ) ↔ ∃x(ψ ∧ φ))
Theorem	19.19 737	Theorem 19.19 of [Margaris] p. 90.
⊢ (φ → ∀xφ)    ⇒   ⊢ (∀x(φ ↔ ψ) → (φ ↔ ∃xψ))
Theorem	19.21 738	Theorem 19.21 of [Margaris] p. 90. The hypothesis can be thought of as "x is not free in φ".
⊢ (φ → ∀xφ)    ⇒   ⊢ (∀x(φ → ψ) ↔ (φ → ∀xψ))
Theorem	stdpc5 739	An axiom of standard predicate calculus. Axiom 5 of [Mendelson] p. 59. The hypothesis (φ → ∀xφ) can be thought of as "x is not free in φ". With this convention, the meaning of "not free" is less restrictive than the usual textbook definition; for example x would not (for us) be free in x = x since (by eqid 810 and hbth 697) we can prove (x = x → ∀xx = x).
⊢ (φ → ∀xφ)    ⇒   ⊢ (∀x(φ → ψ) → (φ → ∀xψ))
Theorem	19.21ai 740	Inference from Theorem 19.21 of [Margaris] p. 90.
⊢ (φ → ∀xφ)    &   ⊢ (φ → ψ)    ⇒   ⊢ (φ → ∀xψ)
Theorem	19.21ad 741	Deduction from Theorem 19.21 of [Margaris] p. 90.
⊢ (φ → ∀xφ)    &   ⊢ (ψ → ∀xψ)    &   ⊢ (φ → (ψ → χ))    ⇒   ⊢ (φ → (ψ → ∀xχ))
Theorem	19.21bi 742	Inference from Theorem 19.21 of [Margaris] p. 90.
⊢ (φ → ∀xψ)    ⇒   ⊢ (φ → ψ)
Theorem	19.21bbi 743	Inference removing double quantifier.
⊢ (φ → ∀x∀yψ)    ⇒   ⊢ (φ → ψ)
Theorem	19.22d 744	Deduction from Theorem 19.22 of [Margaris] p. 90.
⊢ (φ → ∀xφ)    &   ⊢ (φ → (ψ → χ))    ⇒   ⊢ (φ → (∃xψ → ∃xχ))
Theorem	19.23 745	Theorem 19.23 of [Margaris] p. 90.
⊢ (ψ → ∀xψ)    ⇒   ⊢ (∀x(φ → ψ) ↔ (∃xφ → ψ))
Theorem	19.23ai 746	Inference from Theorem 19.23 of [Margaris] p. 90.
⊢ (ψ → ∀xψ)    &   ⊢ (φ → ψ)    ⇒   ⊢ (∃xφ → ψ)
Theorem	19.23bi 747	Inference from Theorem 19.23 of [Margaris] p. 90.
⊢ (∃xφ → ψ)    ⇒   ⊢ (φ → ψ)
Theorem	19.23ad 748	Deduction from Theorem 19.23 of [Margaris] p. 90.
⊢ (φ → ∀xφ)    &   ⊢ (χ → ∀xχ)    &   ⊢ (φ → (ψ → χ))    ⇒   ⊢ (φ → (∃xψ → χ))
Theorem	19.26 749	Theorem 19.26 of [Margaris] p. 90.
⊢ (∀x(φ ∧ ψ) ↔ (∀xφ ∧ ∀xψ))
Theorem	19.27 750	Theorem 19.27 of [Margaris] p. 90.
⊢ (ψ → ∀xψ)    ⇒   ⊢ (∀x(φ ∧ ψ) ↔ (∀xφ ∧ ψ))
Theorem	19.28 751	Theorem 19.28 of [Margaris] p. 90.
⊢ (φ → ∀xφ)    ⇒   ⊢ (∀x(φ ∧ ψ) ↔ (φ ∧ ∀xψ))
Theorem	19.29 752	Theorem 19.29 of [Margaris] p. 90.
⊢ ((∀xφ ∧ ∃xψ) → ∃x(φ ∧ ψ))
Theorem	19.29r 753	Variation of Theorem 19.29 of [Margaris] p. 90.
⊢ ((∃xφ ∧ ∀xψ) → ∃x(φ ∧ ψ))
Theorem	19.35 754	Theorem 19.35 of [Margaris] p. 90. This theorem is useful for moving an implication (in the form of the right-hand side) into the scope of a single existential quantifier.
⊢ (∃x(φ → ψ) ↔ (∀xφ → ∃xψ))
Theorem	19.35i 755	Inference from Theorem 19.35 of [Margaris] p. 90.
⊢ ∃x(φ → ψ)    ⇒   ⊢ (∀xφ → ∃xψ)
Theorem	19.35ri 756	Inference from Theorem 19.35 of [Margaris] p. 90.
⊢ (∀xφ → ∃xψ)    ⇒   ⊢ ∃x(φ → ψ)
Theorem	19.36 757	Theorem 19.36 of [Margaris] p. 90.
⊢ (ψ → ∀xψ)    ⇒   ⊢ (∃x(φ → ψ) ↔ (∀xφ → ψ))
Theorem	19.36i 758	Inference from Theorem 19.36 of [Margaris] p. 90.
⊢ (ψ → ∀xψ)    &   ⊢ ∃x(φ → ψ)    ⇒   ⊢ (∀xφ → ψ)
Theorem	19.37 759	Theorem 19.37 of [Margaris] p. 90.
⊢ (φ → ∀xφ)    ⇒   ⊢ (∃x(φ → ψ) ↔ (φ → ∃xψ))
Theorem	19.38 760	Theorem 19.38 of [Margaris] p. 90.
⊢ ((∃xφ → ∀xψ) → ∀x(φ → ψ))
Theorem	19.39 761	Theorem 19.39 of [Margaris] p. 90.
⊢ ((∃xφ → ∃xψ) → ∃x(φ → ψ))
Theorem	19.24 762	Theorem 19.24 of [Margaris] p. 90.
⊢ ((∀xφ → ∀xψ) → ∃x(φ → ψ))
Theorem	19.25 763	Theorem 19.25 of [Margaris] p. 90.
⊢ (∀y∃x(φ → ψ) → (∃y∀xφ → ∃y∃xψ))
Theorem	19.30 764	Theorem 19.30 of [Margaris] p. 90.
⊢ (∀x(φ ∨ ψ) → (∀xφ ∨ ∃xψ))
Theorem	19.32 765	Theorem 19.32 of [Margaris] p. 90.
⊢ (φ → ∀xφ)    ⇒   ⊢ (∀x(φ ∨ ψ) ↔ (φ ∨ ∀xψ))
Theorem	19.31 766	Theorem 19.31 of [Margaris] p. 90.
⊢ (ψ → ∀xψ)    ⇒   ⊢ (∀x(φ ∨ ψ) ↔ (∀xφ ∨ ψ))
Theorem	19.43 767	Theorem 19.43 of [Margaris] p. 90.
⊢ (∃x(φ ∨ ψ) ↔ (∃xφ ∨ ∃xψ))
Theorem	19.44 768	Theorem 19.44 of [Margaris] p. 90.
⊢ (ψ → ∀xψ)    ⇒   ⊢ (∃x(φ ∨ ψ) ↔ (∃xφ ∨ ψ))
Theorem	19.45 769	Theorem 19.45 of [Margaris] p. 90.
⊢ (φ → ∀xφ)    ⇒   ⊢ (∃x(φ ∨ ψ) ↔ (φ ∨ ∃xψ))
Theorem	19.33 770	Theorem 19.33 of [Margaris] p. 90.
⊢ ((∀xφ ∨ ∀xψ) → ∀x(φ ∨ ψ))
Theorem	19.33b 771	The antecedent provides a condition implying the converse of 19.33 770. Compare Theorem 19.33 of [Margaris] p. 90.
⊢ (¬ (∃xφ ∧ ∃xψ) → (∀x(φ ∨ ψ) ↔ (∀xφ ∨ ∀xψ)))
Theorem	19.34 772	Theorem 19.34 of [Margaris] p. 90.
⊢ ((∀xφ ∨ ∃xψ) → ∃x(φ ∨ ψ))
Theorem	19.40 773	Theorem 19.40 of [Margaris] p. 90.
⊢ (∃x(φ ∧ ψ) → (∃xφ ∧ ∃xψ))
Theorem	19.41 774	Theorem 19.41 of [Margaris] p. 90.
⊢ (ψ → ∀xψ)    ⇒   ⊢ (∃x(φ ∧ ψ) ↔ (∃xφ ∧ ψ))
Theorem	19.42 775	Theorem 19.42 of [Margaris] p. 90.
⊢ (φ → ∀xφ)    ⇒   ⊢ (∃x(φ ∧ ψ) ↔ (φ ∧ ∃xψ))
Theorem	excom13 776	Swap 1st and 3rd existential quantifiers.
⊢ (∃x∃y∃zφ ↔ ∃z∃y∃xφ)
Theorem	exrot3 777	Rotate existential quantifiers.
⊢ (∃x∃y∃zφ ↔ ∃y∃z∃xφ)
Theorem	exrot4 778	Rotate existential quantifiers twice.
⊢ (∃x∃y∃z∃wφ ↔ ∃z∃w∃x∃yφ)
Theorem	nex 779	Generalization rule for negated wff.
⊢ ¬ φ    ⇒   ⊢ ¬ ∃xφ
Theorem	nexd 780	Deduction for generalization rule for negated wff.
⊢ (φ → ∀xφ)    &   ⊢ (φ → ¬ ψ)    ⇒   ⊢ (φ → ¬ ∃xψ)
Theorem	hbim1 781	A closed form of hbim 702.
⊢ (φ → ∀xφ)    &   ⊢ (φ → (ψ → ∀xψ))    ⇒   ⊢ ((φ → ψ) → ∀x(φ → ψ))
Theorem	biald 782	Formula-building rule for universal quantifier (deduction rule).
⊢ (φ → ∀xφ)    &   ⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (φ → (∀xψ ↔ ∀xχ))
Theorem	biexd 783	Formula-building rule for existential quantifier (deduction rule).
⊢ (φ → ∀xφ)    &   ⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (φ → (∃xψ ↔ ∃xχ))
Theorem	exan 784	Place a conjunct in the scope of an existential quantifier.
⊢ (∃xφ ∧ ψ)    ⇒   ⊢ ∃x(φ ∧ ψ)
Theorem	albi 785	Split biconditional and distribute quantifier.
⊢ (∀x(φ ↔ ψ) ↔ (∀x(φ → ψ) ∧ ∀x(ψ → φ)))
Theorem	hbnd 786	A deduction form of bound-variable hypothesis builder hbne 699.
⊢ (φ → ∀xφ)    &   ⊢ (φ → (ψ → ∀xψ))    ⇒   ⊢ (φ → (¬ ψ → ∀x ¬ ψ))
Theorem	hbimd 787	Deduction form of bound-variable hypothesis builder hbim 702.
⊢ (φ → ∀xφ)    &   ⊢ (φ → (ψ → ∀xψ))    &   ⊢ (φ → (χ → ∀xχ))    ⇒   ⊢ (φ → ((ψ → χ) → ∀x(ψ → χ)))
Theorem	hband 788	Deduction form of bound-variable hypothesis builder hban 704.
⊢ (φ → (ψ → ∀xψ))    &   ⊢ (φ → (χ → ∀xχ))    ⇒   ⊢ (φ → ((ψ ∧ χ) → ∀x(ψ ∧ χ)))
Theorem	hbbid 789	Deduction form of bound-variable hypothesis builder hbbi 705.
⊢ (φ → ∀xφ)    &   ⊢ (φ → (ψ → ∀xψ))    &   ⊢ (φ → (χ → ∀xχ))    ⇒   ⊢ (φ → ((ψ ↔ χ) → ∀x(ψ ↔ χ)))
Theorem	hbald 790	Deduction form of bound-variable hypothesis builder hbal 700.
⊢ (φ → ∀yφ)    &   ⊢ (φ → (ψ → ∀xψ))    ⇒   ⊢ (φ → (∀yψ → ∀x∀yψ))
Theorem	hbexd 791	Deduction form of bound-variable hypothesis builder hbex 701.
⊢ (φ → ∀yφ)    &   ⊢ (φ → (ψ → ∀xψ))    ⇒   ⊢ (φ → (∃yψ → ∀x∃yψ))
Theorem	19.21g 792	Closed form of Theorem 19.21 of [Margaris] p. 90.
⊢ (∀x(φ → ∀xφ) → (∀x(φ → ψ) ↔ (φ → ∀xψ)))
Theorem	exintr 793	Introduce a conjunct in the scope of an existential quantifier.
⊢ (∀x(φ → ψ) → (∃xφ → ∃x(φ ∧ ψ)))
Theorem	aaan 794	Rearrange universal quantifiers.
⊢ (φ → ∀yφ)    &   ⊢ (ψ → ∀xψ)    ⇒   ⊢ (∀x∀y(φ ∧ ψ) ↔ (∀xφ ∧ ∀yψ))
Theorem	eeor 795	Rearrange existential quantifiers.
⊢ (φ → ∀yφ)    &   ⊢ (ψ → ∀xψ)    ⇒   ⊢ (∃x∃y(φ ∨ ψ) ↔ (∃xφ ∨ ∃yψ))
Theorem	qexmid 796	Quantified "excluded middle". Exercise 9.2a of Boolos, p. 111, Computability and Logic.
⊢ ∃x(φ → ∀xφ)
Syntax	weq 797	Extend wff definition to include atomic formulas using the equality predicate.
wff x = y
Axiom	ax-8 798	Axiom of Equality. One of the 5 equality axioms of predicate calculus. This is similar to, but not quite, a transitive law for equality (proved later as eqt 814). Axiom scheme C8' in [Megill] p. 448 (p. 16 of the preprint). Also appears as Axiom C7 of [Monk2] p. 105. Axioms ax-8 798 through ax-16 922 are the axioms having to do with equality, substitution, and logical properties of our binary predicate ∈ (which later in set theory will mean "is a member of"). Note that all axioms except ax-16 922 and ax-17 925 are still valid even when x, y, and z are replaced with the same variable because they do not have any distinct variable (Metamath's $d) restrictions. Distinct variable restrictions are required for ax-16 922 and ax-17 925 only.
⊢ (x = y → (x = z → y = z))
Axiom	ax-9 799	Axiom of Existence. One of the 5 equality axioms of equality in predicate calculus. This axiom in effect tells us that at least one thing exists. In this form (not requiring x and y to be distinct) it was used in an axiom system of Tarski (see Axiom B7' in footnote 1 of [KalishMontague] p. 81.) It is equivalent to axiom scheme C10' in [Megill] p. 448 (p. 16 of the preprint); the equivalence is established by ax9 807 and ax9a 808. A more convenient form of this axiom is a9e 809.
⊢ ¬ ∀x ¬ x = y
Axiom	ax-10 800	Axiom of Quantifier Substitution. One of the 5 equality axioms of predicate calculus. This is a technical axiom wherein the antecedent is true only if x and y are the same variable, and in that case it doesn't matter which one you use in a quantifier. Axiom scheme C11' in [Megill] p. 448 (p. 16 of the preprint). It apparently does not otherwise appear in the literature but is easily proved from textbook predicate calculus by cases. (Strictly speaking, the antecedent is also true when x and y are different variables in the case of a one-element domain of discourse, but then the consequent is also true in a one-element domain. For compatibility with traditional predicate calculus all our predicate calculus axioms hold in a one-element domain, but this becomes unimportant in set theory where we show in dtru 1889 that at least 2 things exist.)
⊢ (∀x x = y → (∀xφ → ∀yφ))