P. 366 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 36501-36600   *Has distinct variable group(s)

Type	Label	Description
Statement
Axiom	ax-frege31 36501	ph cannot be denied and (at the same time ) -. -. ph affirmed. Duplex negatio affirmat. The denial of the denial is affirmation. Identical to notnot2 116. Axiom 31 of [Frege1879] p. 44. (Contributed by RP, 24-Dec-2019.) (New usage is discouraged.)
|- ( -. -. ph -> ph )
Theorem	frege32 36502	Deduce con1 133 from con3 141. Proposition 32 of [Frege1879] p. 44. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( ( ( -. ph -> ps ) -> ( -. ps -> -. -. ph ) ) -> ( ( -. ph -> ps ) -> ( -. ps -> ph ) ) )
Theorem	frege33 36503	If ph or ps takes place, then ps or ph takes place. Identical to con1 133. Proposition 33 of [Frege1879] p. 44. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( ( -. ph -> ps ) -> ( -. ps -> ph ) )
Theorem	frege34 36504	If as a conseqence of the occurence of the circumstance ph, when the obstacle ps is removed, ch takes place, then from the circumstance that ch does not take place while ph occurs the occurence of the obstacle ps can be inferred. Closed form of con1d 129. Proposition 34 of [Frege1879] p. 45. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( ( ph -> ( -. ps -> ch ) ) -> ( ph -> ( -. ch -> ps ) ) )
Theorem	frege35 36505	Commuted, closed form of con1d 129. Proposition 35 of [Frege1879] p. 45. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( ( ph -> ( -. ps -> ch ) ) -> ( -. ch -> ( ph -> ps ) ) )
Theorem	frege36 36506	The case in which ps is denied, -. ph is affirmed, and ph is affirmed does not occur. If ph occurs, then (at least) one of the two, ph or ps, takes place (no matter what ps might be). Identical to pm2.24 112. Proposition 36 of [Frege1879] p. 45. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( ph -> ( -. ph -> ps ) )
Theorem	frege37 36507	If ch is a necessary consequence of the occurrence of ps or ph, then ch is a necessary consequence of ph alone. Similar to a closed form of orcs 401. Proposition 37 of [Frege1879] p. 46. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( ( ( -. ph -> ps ) -> ch ) -> ( ph -> ch ) )
Theorem	frege38 36508	Identical to pm2.21 111. Proposition 38 of [Frege1879] p. 46. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( -. ph -> ( ph -> ps ) )
Theorem	frege39 36509	Syllogism between pm2.18 113 and pm2.24 112. Proposition 39 of [Frege1879] p. 46. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( ( -. ph -> ph ) -> ( -. ph -> ps ) )
Theorem	frege40 36510	Anything implies pm2.18 113. Proposition 40 of [Frege1879] p. 46. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( -. ph -> ( ( -. ps -> ps ) -> ps ) )
Theorem	axfrege41 36511	Identical to notnot1 126. Axiom 41 of [Frege1879] p. 47. (Contributed by RP, 24-Dec-2019.)
|- ( ph -> -. -. ph )
Axiom	ax-frege41 36512	The affirmation of ph denies the denial of ph. Identical to notnot1 126. Axiom 41 of [Frege1879] p. 47. (Contributed by RP, 24-Dec-2019.) (New usage is discouraged.)
|- ( ph -> -. -. ph )
Theorem	frege42 36513	Not not id 22. Proposition 42 of [Frege1879] p. 47. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- -. -. ( ph -> ph )
Theorem	frege43 36514	If there is a choice only between ph and ph, then ph takes place. Identical to pm2.18 113. Proposition 43 of [Frege1879] p. 47. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( ( -. ph -> ph ) -> ph )
Theorem	frege44 36515	Similar to a commuted pm2.62 416. Proposition 44 of [Frege1879] p. 47. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( ( -. ph -> ps ) -> ( ( ps -> ph ) -> ph ) )
Theorem	frege45 36516	Deduce pm2.6 175 from con1 133. Proposition 45 of [Frege1879] p. 47. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( ( ( -. ph -> ps ) -> ( -. ps -> ph ) ) -> ( ( -. ph -> ps ) -> ( ( ph -> ps ) -> ps ) ) )
Theorem	frege46 36517	If ps holds when ph occurs as well as when ph does not occur, then ps holds. If ps or ph occurs and if the occurences of ph has ps as a necessary consequence, then ps takes place. Identical to pm2.6 175. Proposition 46 of [Frege1879] p. 48. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( ( -. ph -> ps ) -> ( ( ph -> ps ) -> ps ) )
Theorem	frege47 36518	Deduce consequence follows from either path implied by a disjunction. If ph, as well as ps is sufficient condition for ch and ps or ph takes place, then the proposition ch holds. Proposition 47 of [Frege1879] p. 48. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( ( -. ph -> ps ) -> ( ( ps -> ch ) -> ( ( ph -> ch ) -> ch ) ) )
Theorem	frege48 36519	Closed form of syllogism with internal disjunction. If ph is a sufficient condition for the occurence of ch or ps and if ch, as well as ps, is a sufficient condition for th, then ph is a sufficient condition for th. See application in frege101 36631. Proposition 48 of [Frege1879] p. 49. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( ( ph -> ( -. ps -> ch ) ) -> ( ( ch -> th ) -> ( ( ps -> th ) -> ( ph -> th ) ) ) )
Theorem	frege49 36520	Closed form of deduction with disjunction. Proposition 49 of [Frege1879] p. 49. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( ( -. ph -> ps ) -> ( ( ph -> ch ) -> ( ( ps -> ch ) -> ch ) ) )
Theorem	frege50 36521	Closed form of jaoi 386. Proposition 50 of [Frege1879] p. 49. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( ( ph -> ps ) -> ( ( ch -> ps ) -> ( ( -. ph -> ch ) -> ps ) ) )
Theorem	frege51 36522	Compare with jaod 387. Proposition 51 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( ( ph -> ( ps -> ch ) ) -> ( ( th -> ch ) -> ( ph -> ( ( -. ps -> th ) -> ch ) ) ) )
21.25.3.5  _Begriffsschrift_ Chapter II with logical equivalence Here we leverage df-ifp 984 to partition a wff into two that are disjoint with the selector wff. Thus if we are given |- ( ph <-> if- ( ps , ch , th ) ) then we replace the concept (illegal in our notation ) ( ph ` ps ) with if- ( ps , ch , th ) to reason about the values of the "function." Likewise, we replace the similarly illegal concept A. ps ph with ( ch /\ th ).
Theorem	axfrege52a 36523	Justification for ax-frege52a 36524. (Contributed by RP, 17-Apr-2020.)
|- ( ( ph <-> ps ) -> (if- ( ph , th , ch ) -> if- ( ps , th , ch ) ) )
Axiom	ax-frege52a 36524	The case when the content of ph is identical with the content of ps and in which a proposition controlled by an element for which we substitute the content of ph is affirmed ( in this specific case the identity logical funtion ) and the same proposition, this time where we subsituted the content of ps, is denied does not take place. Part of Axiom 52 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (New usage is discouraged.)
|- ( ( ph <-> ps ) -> (if- ( ph , th , ch ) -> if- ( ps , th , ch ) ) )
Theorem	frege52aid 36525	The case when the content of ph is identical with the content of ps and in which ph is affirmed and ps is denied does not take place. Identical to biimp 198. Part of Axiom 52 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( ( ph <-> ps ) -> ( ph -> ps ) )
Theorem	frege53aid 36526	Specialization of frege53a 36527. Proposition 53 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( ph -> ( ( ph <-> ps ) -> ps ) )
Theorem	frege53a 36527	Lemma for frege55a 36535. Proposition 53 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- (if- ( ph , th , ch ) -> ( ( ph <-> ps ) -> if- ( ps , th , ch ) ) )
Theorem	axfrege54a 36528	Justification for ax-frege54a 36529. Identical to biid 244. (Contributed by RP, 24-Dec-2019.)
|- ( ph <-> ph )
Axiom	ax-frege54a 36529	Reflexive equality of wffs. The content of ph is identical with the content of ph. Part of Axiom 54 of [Frege1879] p. 50. Identical to biid 244. (Contributed by RP, 24-Dec-2019.) (New usage is discouraged.)
|- ( ph <-> ph )
Theorem	frege54cor0a 36530	Synonym for logical equivalence. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( ( ps <-> ph ) <-> if- ( ps , ph , -. ph ) )
Theorem	frege54cor1a 36531	Reflexive equality. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- if- ( ph , ph , -. ph )
Theorem	frege55aid 36532	Lemma for frege57aid 36539. Core proof of Proposition 55 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.)
|- ( ( ph <-> ps ) -> ( ps <-> ph ) )
Theorem	frege55lem1a 36533	Necessary deduction regarding substitution of value in equality. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( ( ta -> if- ( ps , ph , -. ph ) ) -> ( ta -> ( ps <-> ph ) ) )
Theorem	frege55lem2a 36534	Core proof of Proposition 55 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( ( ph <-> ps ) -> if- ( ps , ph , -. ph ) )
Theorem	frege55a 36535	Proposition 55 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( ( ph <-> ps ) -> if- ( ps , ph , -. ph ) )
Theorem	frege55cor1a 36536	Proposition 55 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( ( ph <-> ps ) -> ( ps <-> ph ) )
Theorem	frege56aid 36537	Lemma for frege57aid 36539. Proposition 56 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( ( ( ph <-> ps ) -> ( ph -> ps ) ) -> ( ( ps <-> ph ) -> ( ph -> ps ) ) )
Theorem	frege56a 36538	Proposition 56 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( ( ( ph <-> ps ) -> (if- ( ph , ch , th ) -> if- ( ps , ch , th ) ) ) -> ( ( ps <-> ph ) -> (if- ( ph , ch , th ) -> if- ( ps , ch , th ) ) ) )
Theorem	frege57aid 36539	This is the all imporant formula which allows us to apply Frege-style definitions and explore their consequences. A closed form of biimpri 211. Proposition 57 of [Frege1879] p. 51. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( ( ph <-> ps ) -> ( ps -> ph ) )
Theorem	frege57a 36540	Analogue of frege57aid 36539. Proposition 57 of [Frege1879] p. 51. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( ( ph <-> ps ) -> (if- ( ps , ch , th ) -> if- ( ph , ch , th ) ) )
Theorem	axfrege58a 36541	Identical to anifp 991. Justification for ax-frege58a 36542. (Contributed by RP, 28-Mar-2020.)
|- ( ( ps /\ ch ) -> if- ( ph , ps , ch ) )
Axiom	ax-frege58a 36542	If A. x ph is affirmed, [ y / x ] ph cannot be denied. Identical to stdpc4 2202. Axiom 58 of [Frege1879] p. 51. (Contributed by RP, 28-Mar-2020.) (New usage is discouraged.)
|- ( ( ps /\ ch ) -> if- ( ph , ps , ch ) )
Theorem	frege58acor 36543	Lemma for frege59a 36544. (Contributed by RP, 17-Apr-2020.) (Proof modification is discouraged.)
|- ( ( ( ps -> ch ) /\ ( th -> ta ) ) -> (if- ( ph , ps , th ) -> if- ( ph , ch , ta ) ) )
Theorem	frege59a 36544	A kind of Aristotelian inference. Namely Felapton or Fesapo. Proposition 59 of [Frege1879] p. 51. Note: in the Bauer-Meenfelberg translation published in van Heijenoort's collection From Frege to Goedel, this proof has the frege12 36480 incorrectly referenced where frege30 36499 is in the original. (Contributed by RP, 17-Apr-2020.) (Proof modification is discouraged.)
|- (if- ( ph , ps , th ) -> ( -. if- ( ph , ch , ta ) -> -. ( ( ps -> ch ) /\ ( th -> ta ) ) ) )
Theorem	frege60a 36545	Swap antecedents of ax-frege58a 36542. Proposition 60 of [Frege1879] p. 52. (Contributed by RP, 17-Apr-2020.) (Proof modification is discouraged.)
|- ( ( ( ps -> ( ch -> th ) ) /\ ( ta -> ( et -> ze ) ) ) -> (if- ( ph , ch , et ) -> (if- ( ph , ps , ta ) -> if- ( ph , th , ze ) ) ) )
Theorem	frege61a 36546	Lemma for frege65a 36550. Proposition 61 of [Frege1879] p. 52. (Contributed by RP, 17-Apr-2020.) (Proof modification is discouraged.)
|- ( (if- ( ph , ps , ch ) -> th ) -> ( ( ps /\ ch ) -> th ) )
Theorem	frege62a 36547	A kind of Aristotelian inference. This judgement replaces the mode of inference barbara 2412 when the minor premise has a particular context. Proposition 62 of [Frege1879] p. 52. (Contributed by RP, 17-Apr-2020.) (Proof modification is discouraged.)
|- (if- ( ph , ps , th ) -> ( ( ( ps -> ch ) /\ ( th -> ta ) ) -> if- ( ph , ch , ta ) ) )
Theorem	frege63a 36548	Proposition 63 of [Frege1879] p. 52. (Contributed by RP, 17-Apr-2020.) (Proof modification is discouraged.)
|- (if- ( ph , ps , th ) -> ( et -> ( ( ( ps -> ch ) /\ ( th -> ta ) ) -> if- ( ph , ch , ta ) ) ) )
Theorem	frege64a 36549	Lemma for frege65a 36550. Proposition 64 of [Frege1879] p. 53. (Contributed by RP, 17-Apr-2020.) (Proof modification is discouraged.)
|- ( (if- ( ph , ps , ta ) -> if- ( si , ch , et ) ) -> ( ( ( ch -> th ) /\ ( et -> ze ) ) -> (if- ( ph , ps , ta ) -> if- ( si , th , ze ) ) ) )
Theorem	frege65a 36550	A kind of Aristotelian inference. This judgement replaces the mode of inference barbara 2412 when the minor premise has a general context. Proposition 65 of [Frege1879] p. 53. (Contributed by RP, 17-Apr-2020.) (Proof modification is discouraged.)
|- ( ( ( ps -> ch ) /\ ( ta -> et ) ) -> ( ( ( ch -> th ) /\ ( et -> ze ) ) -> (if- ( ph , ps , ta ) -> if- ( ph , th , ze ) ) ) )
Theorem	frege66a 36551	Swap antecedents of frege65a 36550. Proposition 66 of [Frege1879] p. 54. (Contributed by RP, 17-Apr-2020.) (Proof modification is discouraged.)
|- ( ( ( ch -> th ) /\ ( et -> ze ) ) -> ( ( ( ps -> ch ) /\ ( ta -> et ) ) -> (if- ( ph , ps , ta ) -> if- ( ph , th , ze ) ) ) )
Theorem	frege67a 36552	Lemma for frege68a 36553. Proposition 67 of [Frege1879] p. 54. (Contributed by RP, 17-Apr-2020.) (Proof modification is discouraged.)
|- ( ( ( ( ps /\ ch ) <-> th ) -> ( th -> ( ps /\ ch ) ) ) -> ( ( ( ps /\ ch ) <-> th ) -> ( th -> if- ( ph , ps , ch ) ) ) )
Theorem	frege68a 36553	Combination of applying a definition and applying it to a specific instance. Proposition 68 of [Frege1879] p. 54. (Contributed by RP, 17-Apr-2020.) (Proof modification is discouraged.)
|- ( ( ( ps /\ ch ) <-> th ) -> ( th -> if- ( ph , ps , ch ) ) )
21.25.3.6  _Begriffsschrift_ Chapter II with equivalence of sets
Theorem	axfrege52c 36554	Justification for ax-frege52c 36555. (Contributed by RP, 24-Dec-2019.)
|- ( A = B -> ( [. A / x ]. ph -> [. B / x ]. ph ) )
Axiom	ax-frege52c 36555	One side of dfsbcq 3257. Part of Axiom 52 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (New usage is discouraged.)
|- ( A = B -> ( [. A / x ]. ph -> [. B / x ]. ph ) )
Theorem	frege52b 36556	The case when the content of x is identical with the content of y and in which a proposition controlled by an element for which we substitute the content of x is affirmed and the same proposition, this time where we subsitute the content of y, is denied does not take place. In [ x / z ] ph, x can also occur in other than the argument ( z) places. Hence x may still be contained in [ y / z ] ph. Part of Axiom 52 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( x = y -> ( [ x / z ] ph -> [ y / z ] ph ) )
Theorem	frege53b 36557	Lemma for frege102 (via frege92 36622). Proposition 53 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( [ x / y ] ph -> ( x = z -> [ z / y ] ph ) )
Theorem	axfrege54c 36558	Reflexive equality of classes. Identical to eqid 2471. Justification for ax-frege54c 36559. (Contributed by RP, 24-Dec-2019.)
|- A = A
Axiom	ax-frege54c 36559	Reflexive equality of sets (as classes). Part of Axiom 54 of [Frege1879] p. 50. Identical to eqid 2471. (Contributed by RP, 24-Dec-2019.) (New usage is discouraged.)
|- A = A
Theorem	frege54b 36560	Reflexive equality of sets. The content of x is identical with the content of x. Part of Axiom 54 of [Frege1879] p. 50. Slightly specialized version of eqid 2471. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- x = x
Theorem	frege54cor1b 36561	Reflexive equality. (Contributed by RP, 24-Dec-2019.)
|- [ x / y ] y = x
Theorem	frege55lem1b 36562*	Necessary deduction regarding substitution of value in equality. (Contributed by RP, 24-Dec-2019.)
|- ( ( ph -> [ x / y ] y = z ) -> ( ph -> x = z ) )
Theorem	frege55lem2b 36563	Lemma for frege55b 36564. Core proof of Proposition 55 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( x = y -> [ y / z ] z = x )
Theorem	frege55b 36564	Lemma for frege57b 36566. Proposition 55 of [Frege1879] p. 50. Note that eqtr2 2491 incorporates eqcom 2478 which is stronger than this proposition which is identical to equcomi 1869. Is is possible that Frege tricked himself into assuming what he was out to prove? (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( x = y -> y = x )
Theorem	frege56b 36565	Lemma for frege57b 36566. Proposition 56 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( ( x = y -> ( [ x / z ] ph -> [ y / z ] ph ) ) -> ( y = x -> ( [ x / z ] ph -> [ y / z ] ph ) ) )
Theorem	frege57b 36566	Analogue of frege57aid 36539. Proposition 57 of [Frege1879] p. 51. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( x = y -> ( [ y / z ] ph -> [ x / z ] ph ) )
Theorem	axfrege58b 36567	If A. x ph is affirmed, [ y / x ] ph cannot be denied. Identical to stdpc4 2202. Justification for ax-frege58b 36568. (Contributed by RP, 28-Mar-2020.)
|- ( A. x ph -> [ y / x ] ph )
Axiom	ax-frege58b 36568	If A. x ph is affirmed, [ y / x ] ph cannot be denied. Identical to stdpc4 2202. Axiom 58 of [Frege1879] p. 51. (Contributed by RP, 28-Mar-2020.) (New usage is discouraged.)
|- ( A. x ph -> [ y / x ] ph )
Theorem	frege58bid 36569	If A. x ph is affirmed, ph cannot be denied. Identical to sp 1957. See ax-frege58b 36568 and frege58c 36588 for versions which more closely track the original. Axiom 58 of [Frege1879] p. 51. (Contributed by RP, 28-Mar-2020.) (Proof modification is discouraged.)
|- ( A. x ph -> ph )
Theorem	frege58bcor 36570	Lemma for frege59b 36571. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( A. x ( ph -> ps ) -> ( [ y / x ] ph -> [ y / x ] ps ) )
Theorem	frege59b 36571	A kind of Aristotelian inference. Namely Felapton or Fesapo. Proposition 59 of [Frege1879] p. 51. Note: in the Bauer-Meenfelberg translation published in van Heijenoort's collection From Frege to Goedel, this proof has the frege12 36480 incorrectly referenced where frege30 36499 is in the original. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( [ x / y ] ph -> ( -. [ x / y ] ps -> -. A. y ( ph -> ps ) ) )
Theorem	frege60b 36572	Swap antecedents of ax-frege58b 36568. Proposition 60 of [Frege1879] p. 52. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( A. x ( ph -> ( ps -> ch ) ) -> ( [ y / x ] ps -> ( [ y / x ] ph -> [ y / x ] ch ) ) )
Theorem	frege61b 36573	Lemma for frege65b 36577. Proposition 61 of [Frege1879] p. 52. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( ( [ x / y ] ph -> ps ) -> ( A. y ph -> ps ) )
Theorem	frege62b 36574	A kind of Aristotelian inference. This judgement replaces the mode of inference barbara 2412 when the minor premise has a particular context. Proposition 62 of [Frege1879] p. 52. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( [ x / y ] ph -> ( A. y ( ph -> ps ) -> [ x / y ] ps ) )
Theorem	frege63b 36575	Lemma for frege91 36621. Proposition 63 of [Frege1879] p. 52. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( [ x / y ] ph -> ( ps -> ( A. y ( ph -> ch ) -> [ x / y ] ch ) ) )
Theorem	frege64b 36576	Lemma for frege65b 36577. Proposition 64 of [Frege1879] p. 53. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( ( [ x / y ] ph -> [ z / y ] ps ) -> ( A. y ( ps -> ch ) -> ( [ x / y ] ph -> [ z / y ] ch ) ) )
Theorem	frege65b 36577	A kind of Aristotelian inference. This judgement replaces the mode of inference barbara 2412 when the minor premise has a general context. Proposition 65 of [Frege1879] p. 53. In Frege care is taken to point out that the variables in the first clauses are independent of each other and of the final term so another valid translation could be : |- ( A. x ( [ x / a ] ph -> [ x / b ] ps ) -> ( A. y ( [ y / b ] ps -> [ y / c ] ch ) -> ( [ z / a ] ph -> [ z / c ] ch ) ) ). But that is perhaps too pedantic a translation for this exploration. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( A. x ( ph -> ps ) -> ( A. x ( ps -> ch ) -> ( [ y / x ] ph -> [ y / x ] ch ) ) )
Theorem	frege66b 36578	Swap antecedents of frege65b 36577. Proposition 66 of [Frege1879] p. 54. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( A. x ( ph -> ps ) -> ( A. x ( ch -> ph ) -> ( [ y / x ] ch -> [ y / x ] ps ) ) )
Theorem	frege67b 36579	Lemma for frege68b 36580. Proposition 67 of [Frege1879] p. 54. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( ( ( A. x ph <-> ps ) -> ( ps -> A. x ph ) ) -> ( ( A. x ph <-> ps ) -> ( ps -> [ y / x ] ph ) ) )
Theorem	frege68b 36580	Combination of applying a definition and applying it to a specific instance. Proposition 68 of [Frege1879] p. 54. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( ( A. x ph <-> ps ) -> ( ps -> [ y / x ] ph ) )
21.25.3.7  _Begriffsschrift_ Chapter II with equivalence of classes (where they are sets)
Theorem	frege53c 36581	Proposition 53 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( [. A / x ]. ph -> ( A = B -> [. B / x ]. ph ) )
Theorem	frege54cor1c 36582*	Reflexive equality. (Contributed by RP, 24-Dec-2019.) (Revised by RP, 25-Apr-2020.)
|- A e. C   =>    |- [. A / x ]. x = A
Theorem	frege55lem1c 36583*	Necessary deduction regarding substitution of value in equality. (Contributed by RP, 24-Dec-2019.)
|- ( ( ph -> [. A / x ]. x = B ) -> ( ph -> A = B ) )
Theorem	frege55lem2c 36584*	Core proof of Proposition 55 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( x = A -> [. A / z ]. z = x )
Theorem	frege55c 36585	Proposition 55 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( x = A -> A = x )
Theorem	frege56c 36586*	Lemma for frege57c 36587. Proposition 56 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- B e. C   =>    |- ( ( A = B -> ( [. A / x ]. ph -> [. B / x ]. ph ) ) -> ( B = A -> ( [. A / x ]. ph -> [. B / x ]. ph ) ) )
Theorem	frege57c 36587*	Swap order of implication in ax-frege52c 36555. Proposition 57 of [Frege1879] p. 51. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- A e. C   =>    |- ( A = B -> ( [. B / x ]. ph -> [. A / x ]. ph ) )
Theorem	frege58c 36588	Principle related to sp 1957. Axiom 58 of [Frege1879] p. 51. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- A e. B   =>    |- ( A. x ph -> [. A / x ]. ph )
Theorem	frege59c 36589	A kind of Aristotelian inference. Proposition 59 of [Frege1879] p. 51. Note: in the Bauer-Meenfelberg translation published in van Heijenoort's collection From Frege to Goedel, this proof has the frege12 36480 incorrectly referenced where frege30 36499 is in the original. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- A e. B   =>    |- ( [. A / x ]. ph -> ( -. [. A / x ]. ps -> -. A. x ( ph -> ps ) ) )
Theorem	frege60c 36590	Swap antecedents of frege58c 36588. Proposition 60 of [Frege1879] p. 52. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- A e. B   =>    |- ( A. x ( ph -> ( ps -> ch ) ) -> ( [. A / x ]. ps -> ( [. A / x ]. ph -> [. A / x ]. ch ) ) )
Theorem	frege61c 36591	Lemma for frege65c 36595. Proposition 61 of [Frege1879] p. 52. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- A e. B   =>    |- ( ( [. A / x ]. ph -> ps ) -> ( A. x ph -> ps ) )
Theorem	frege62c 36592	A kind of Aristotelian inference. This judgement replaces the mode of inference barbara 2412 when the minor premise has a particular context. Proposition 62 of [Frege1879] p. 52. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- A e. B   =>    |- ( [. A / x ]. ph -> ( A. x ( ph -> ps ) -> [. A / x ]. ps ) )
Theorem	frege63c 36593	Analogue of frege63b 36575. Proposition 63 of [Frege1879] p. 52. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- A e. B   =>    |- ( [. A / x ]. ph -> ( ps -> ( A. x ( ph -> ch ) -> [. A / x ]. ch ) ) )
Theorem	frege64c 36594	Lemma for frege65c 36595. Proposition 64 of [Frege1879] p. 53. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- A e. B   =>    |- ( ( [. C / x ]. ph -> [. A / x ]. ps ) -> ( A. x ( ps -> ch ) -> ( [. C / x ]. ph -> [. A / x ]. ch ) ) )
Theorem	frege65c 36595	A kind of Aristotelian inference. This judgement replaces the mode of inference barbara 2412 when the minor premise has a general context. Proposition 65 of [Frege1879] p. 53. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- A e. B   =>    |- ( A. x ( ph -> ps ) -> ( A. x ( ps -> ch ) -> ( [. A / x ]. ph -> [. A / x ]. ch ) ) )
Theorem	frege66c 36596	Swap antecedents of frege65c 36595. Proposition 66 of [Frege1879] p. 54. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- A e. B   =>    |- ( A. x ( ph -> ps ) -> ( A. x ( ch -> ph ) -> ( [. A / x ]. ch -> [. A / x ]. ps ) ) )
Theorem	frege67c 36597	Lemma for frege68c 36598. Proposition 67 of [Frege1879] p. 54. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- A e. B   =>    |- ( ( ( A. x ph <-> ps ) -> ( ps -> A. x ph ) ) -> ( ( A. x ph <-> ps ) -> ( ps -> [. A / x ]. ph ) ) )
Theorem	frege68c 36598	Combination of applying a definition and applying it to a specific instance. Proposition 68 of [Frege1879] p. 54. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- A e. B   =>    |- ( ( A. x ph <-> ps ) -> ( ps -> [. A / x ]. ph ) )
21.25.3.8  _Begriffsschrift_ Chapter III Properties hereditary in a sequence ( R " A ) C_ A means membership in A is hereditary in the sequence dictated by relation R. This differs from the set-theoretic notion that a set is hereditary in a property: that all of its elements have a property and all of their elements have the property and so-on. While the above notation is modern, it is cumbersome in the case when A is complex and to more closely follow Frege, we abbreviate it with new notation R hereditary A. This greatly shortens the statements for frege97 36627 and frege109 36639. dffrege69 36599 through frege75 36605 develop this, but translation to Metamath is pending some decisions. While Frege does not limit discussion to sets, we may have to depart from Frege by limiting R or A to sets when we quantify over all hereditary relations or all classes where membership is hereditary in a sequence dictated by R.
Theorem	dffrege69 36599*	If from the proposition that x has property A it can be inferred generally, whatever x may be, that every result of an application of the procedure R to x has property A, then we say " Property A is hereditary in the R-sequence. Definition 69 of [Frege1879] p. 55. (Contributed by RP, 28-Mar-2020.)
|- ( A. x ( x e. A -> A. y ( x R y -> y e. A ) ) <-> R hereditary A )
Theorem	frege70 36600*	Lemma for frege72 36602. Proposition 70 of [Frege1879] p. 58. (Contributed by RP, 28-Mar-2020.) (Revised by RP, 3-Jul-2020.) (Proof modification is discouraged.)
|- X e. V   =>    |- ( R hereditary A -> ( X e. A -> A. y ( X R y -> y e. A ) ) )