![]() |
Metamath
Proof Explorer Theorem List (p. 55 of 479) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30171) |
![]() (30172-31694) |
![]() (31695-47852) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | reusv2lem5 5401* | Lemma for reusv2 5402. (Contributed by NM, 4-Jan-2013.) (Proof shortened by Mario Carneiro, 19-Nov-2016.) |
⊢ ((∀𝑦 ∈ 𝐵 𝐶 ∈ 𝐴 ∧ 𝐵 ≠ ∅) → (∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶 ↔ ∃!𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 = 𝐶)) | ||
Theorem | reusv2 5402* | Two ways to express single-valuedness of a class expression 𝐶(𝑦) that is constant for those 𝑦 ∈ 𝐵 such that 𝜑. The first antecedent ensures that the constant value belongs to the existential uniqueness domain 𝐴, and the second ensures that 𝐶(𝑦) is evaluated for at least one 𝑦. (Contributed by NM, 4-Jan-2013.) (Proof shortened by Mario Carneiro, 19-Nov-2016.) |
⊢ ((∀𝑦 ∈ 𝐵 (𝜑 → 𝐶 ∈ 𝐴) ∧ ∃𝑦 ∈ 𝐵 𝜑) → (∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝑥 = 𝐶) ↔ ∃!𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝐶))) | ||
Theorem | reusv3i 5403* | Two ways of expressing existential uniqueness via an indirect equality. (Contributed by NM, 23-Dec-2012.) |
⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝑧 → 𝐶 = 𝐷) ⇒ ⊢ (∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝐶) → ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝜑 ∧ 𝜓) → 𝐶 = 𝐷)) | ||
Theorem | reusv3 5404* | Two ways to express single-valuedness of a class expression 𝐶(𝑦). See reusv1 5396 for the connection to uniqueness. (Contributed by NM, 27-Dec-2012.) |
⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝑧 → 𝐶 = 𝐷) ⇒ ⊢ (∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝐶 ∈ 𝐴) → (∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝜑 ∧ 𝜓) → 𝐶 = 𝐷) ↔ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝐶))) | ||
Theorem | eusv4 5405* | Two ways to express single-valuedness of a class expression 𝐵(𝑦). (Contributed by NM, 27-Oct-2010.) |
⊢ 𝐵 ∈ V ⇒ ⊢ (∃!𝑥∃𝑦 ∈ 𝐴 𝑥 = 𝐵 ↔ ∃!𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵) | ||
Theorem | alxfr 5406* | Transfer universal quantification from a variable 𝑥 to another variable 𝑦 contained in expression 𝐴. (Contributed by NM, 18-Feb-2007.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((∀𝑦 𝐴 ∈ 𝐵 ∧ ∀𝑥∃𝑦 𝑥 = 𝐴) → (∀𝑥𝜑 ↔ ∀𝑦𝜓)) | ||
Theorem | ralxfrd 5407* | Transfer universal quantification from a variable 𝑥 to another variable 𝑦 contained in expression 𝐴. (Contributed by NM, 15-Aug-2014.) (Proof shortened by Mario Carneiro, 19-Nov-2016.) (Proof shortened by JJ, 7-Aug-2021.) |
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → 𝐴 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∃𝑦 ∈ 𝐶 𝑥 = 𝐴) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐵 𝜓 ↔ ∀𝑦 ∈ 𝐶 𝜒)) | ||
Theorem | rexxfrd 5408* | Transfer universal quantification from a variable 𝑥 to another variable 𝑦 contained in expression 𝐴. (Contributed by FL, 10-Apr-2007.) (Revised by Mario Carneiro, 15-Aug-2014.) |
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → 𝐴 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∃𝑦 ∈ 𝐶 𝑥 = 𝐴) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐵 𝜓 ↔ ∃𝑦 ∈ 𝐶 𝜒)) | ||
Theorem | ralxfr2d 5409* | Transfer universal quantification from a variable 𝑥 to another variable 𝑦 contained in expression 𝐴. (Contributed by Mario Carneiro, 20-Aug-2014.) |
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↔ ∃𝑦 ∈ 𝐶 𝑥 = 𝐴)) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐵 𝜓 ↔ ∀𝑦 ∈ 𝐶 𝜒)) | ||
Theorem | rexxfr2d 5410* | Transfer universal quantification from a variable 𝑥 to another variable 𝑦 contained in expression 𝐴. (Contributed by Mario Carneiro, 20-Aug-2014.) (Proof shortened by Mario Carneiro, 19-Nov-2016.) |
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↔ ∃𝑦 ∈ 𝐶 𝑥 = 𝐴)) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐵 𝜓 ↔ ∃𝑦 ∈ 𝐶 𝜒)) | ||
Theorem | ralxfrd2 5411* | Transfer universal quantification from a variable 𝑥 to another variable 𝑦 contained in expression 𝐴. Variant of ralxfrd 5407. (Contributed by Alexander van der Vekens, 25-Apr-2018.) |
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → 𝐴 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∃𝑦 ∈ 𝐶 𝑥 = 𝐴) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐵 𝜓 ↔ ∀𝑦 ∈ 𝐶 𝜒)) | ||
Theorem | rexxfrd2 5412* | Transfer existence from a variable 𝑥 to another variable 𝑦 contained in expression 𝐴. Variant of rexxfrd 5408. (Contributed by Alexander van der Vekens, 25-Apr-2018.) |
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → 𝐴 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∃𝑦 ∈ 𝐶 𝑥 = 𝐴) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐵 𝜓 ↔ ∃𝑦 ∈ 𝐶 𝜒)) | ||
Theorem | ralxfr 5413* | Transfer universal quantification from a variable 𝑥 to another variable 𝑦 contained in expression 𝐴. (Contributed by NM, 10-Jun-2005.) (Revised by Mario Carneiro, 15-Aug-2014.) |
⊢ (𝑦 ∈ 𝐶 → 𝐴 ∈ 𝐵) & ⊢ (𝑥 ∈ 𝐵 → ∃𝑦 ∈ 𝐶 𝑥 = 𝐴) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐶 𝜓) | ||
Theorem | ralxfrALT 5414* | Alternate proof of ralxfr 5413 which does not use ralxfrd 5407. (Contributed by NM, 10-Jun-2005.) (Revised by Mario Carneiro, 15-Aug-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑦 ∈ 𝐶 → 𝐴 ∈ 𝐵) & ⊢ (𝑥 ∈ 𝐵 → ∃𝑦 ∈ 𝐶 𝑥 = 𝐴) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐶 𝜓) | ||
Theorem | rexxfr 5415* | Transfer existence from a variable 𝑥 to another variable 𝑦 contained in expression 𝐴. (Contributed by NM, 10-Jun-2005.) (Revised by Mario Carneiro, 15-Aug-2014.) |
⊢ (𝑦 ∈ 𝐶 → 𝐴 ∈ 𝐵) & ⊢ (𝑥 ∈ 𝐵 → ∃𝑦 ∈ 𝐶 𝑥 = 𝐴) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐶 𝜓) | ||
Theorem | rabxfrd 5416* | Membership in a restricted class abstraction after substituting an expression 𝐴 (containing 𝑦) for 𝑥 in the formula defining the class abstraction. (Contributed by NM, 16-Jan-2012.) |
⊢ Ⅎ𝑦𝐵 & ⊢ Ⅎ𝑦𝐶 & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝐴 ∈ 𝐷) & ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜒)) & ⊢ (𝑦 = 𝐵 → 𝐴 = 𝐶) ⇒ ⊢ ((𝜑 ∧ 𝐵 ∈ 𝐷) → (𝐶 ∈ {𝑥 ∈ 𝐷 ∣ 𝜓} ↔ 𝐵 ∈ {𝑦 ∈ 𝐷 ∣ 𝜒})) | ||
Theorem | rabxfr 5417* | Membership in a restricted class abstraction after substituting an expression 𝐴 (containing 𝑦) for 𝑥 in the formula defining the class abstraction. (Contributed by NM, 10-Jun-2005.) |
⊢ Ⅎ𝑦𝐵 & ⊢ Ⅎ𝑦𝐶 & ⊢ (𝑦 ∈ 𝐷 → 𝐴 ∈ 𝐷) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → 𝐴 = 𝐶) ⇒ ⊢ (𝐵 ∈ 𝐷 → (𝐶 ∈ {𝑥 ∈ 𝐷 ∣ 𝜑} ↔ 𝐵 ∈ {𝑦 ∈ 𝐷 ∣ 𝜓})) | ||
Theorem | reuhypd 5418* | A theorem useful for eliminating the restricted existential uniqueness hypotheses in riotaxfrd 7400. (Contributed by NM, 16-Jan-2012.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐵 ∈ 𝐶) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶) → (𝑥 = 𝐴 ↔ 𝑦 = 𝐵)) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ∃!𝑦 ∈ 𝐶 𝑥 = 𝐴) | ||
Theorem | reuhyp 5419* | A theorem useful for eliminating the restricted existential uniqueness hypotheses in reuxfr1 3749. (Contributed by NM, 15-Nov-2004.) |
⊢ (𝑥 ∈ 𝐶 → 𝐵 ∈ 𝐶) & ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶) → (𝑥 = 𝐴 ↔ 𝑦 = 𝐵)) ⇒ ⊢ (𝑥 ∈ 𝐶 → ∃!𝑦 ∈ 𝐶 𝑥 = 𝐴) | ||
Theorem | zfpair 5420 |
The Axiom of Pairing of Zermelo-Fraenkel set theory. Axiom 2 of
[TakeutiZaring] p. 15. In some
textbooks this is stated as a separate
axiom; here we show it is redundant since it can be derived from the
other axioms.
This theorem should not be referenced by any proof other than axprALT 5421. Instead, use zfpair2 5429 below so that the uses of the Axiom of Pairing can be more easily identified. (Contributed by NM, 18-Oct-1995.) (New usage is discouraged.) |
⊢ {𝑥, 𝑦} ∈ V | ||
Theorem | axprALT 5421* | Alternate proof of axpr 5427. (Contributed by NM, 14-Nov-2006.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ∃𝑧∀𝑤((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤 ∈ 𝑧) | ||
Theorem | axprlem1 5422* | Lemma for axpr 5427. There exists a set to which all empty sets belong. (Contributed by Rohan Ridenour, 10-Aug-2023.) (Revised by BJ, 13-Aug-2023.) |
⊢ ∃𝑥∀𝑦(∀𝑧 ¬ 𝑧 ∈ 𝑦 → 𝑦 ∈ 𝑥) | ||
Theorem | axprlem2 5423* | Lemma for axpr 5427. There exists a set to which all sets whose only members are empty sets belong. (Contributed by Rohan Ridenour, 9-Aug-2023.) (Revised by BJ, 13-Aug-2023.) |
⊢ ∃𝑥∀𝑦(∀𝑧 ∈ 𝑦 ∀𝑤 ¬ 𝑤 ∈ 𝑧 → 𝑦 ∈ 𝑥) | ||
Theorem | axprlem3 5424* | Lemma for axpr 5427. Eliminate the antecedent of the relevant replacement instance. (Contributed by Rohan Ridenour, 10-Aug-2023.) |
⊢ ∃𝑧∀𝑤(𝑤 ∈ 𝑧 ↔ ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))) | ||
Theorem | axprlem4 5425* | Lemma for axpr 5427. The first element of the pair is included in any superset of the set whose existence is asserted by the axiom of replacement. (Contributed by Rohan Ridenour, 10-Aug-2023.) (Revised by BJ, 13-Aug-2023.) |
⊢ ((∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) ∧ 𝑤 = 𝑥) → ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))) | ||
Theorem | axprlem5 5426* | Lemma for axpr 5427. The second element of the pair is included in any superset of the set whose existence is asserted by the axiom of replacement. (Contributed by Rohan Ridenour, 10-Aug-2023.) (Revised by BJ, 13-Aug-2023.) |
⊢ ((∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) ∧ 𝑤 = 𝑦) → ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))) | ||
Theorem | axpr 5427* |
Unabbreviated version of the Axiom of Pairing of ZF set theory, derived
as a theorem from the other axioms.
This theorem should not be referenced by any proof. Instead, use ax-pr 5428 below so that the uses of the Axiom of Pairing can be more easily identified. For a shorter proof using ax-ext 2704, see axprALT 5421. (Contributed by NM, 14-Nov-2006.) Remove dependency on ax-ext 2704. (Revised by Rohan Ridenour, 10-Aug-2023.) (Proof shortened by BJ, 13-Aug-2023.) Use ax-pr 5428 instead. (New usage is discouraged.) |
⊢ ∃𝑧∀𝑤((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤 ∈ 𝑧) | ||
Axiom | ax-pr 5428* | The Axiom of Pairing of ZF set theory. It was derived as Theorem axpr 5427 above and is therefore redundant, but we state it as a separate axiom here so that its uses can be identified more easily. (Contributed by NM, 14-Nov-2006.) |
⊢ ∃𝑧∀𝑤((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤 ∈ 𝑧) | ||
Theorem | zfpair2 5429 | Derive the abbreviated version of the Axiom of Pairing from ax-pr 5428. See zfpair 5420 for its derivation from the other axioms. (Contributed by NM, 14-Nov-2006.) |
⊢ {𝑥, 𝑦} ∈ V | ||
Theorem | vsnex 5430 | A singleton built on a setvar is a set. (Contributed by BJ, 15-Jan-2025.) |
⊢ {𝑥} ∈ V | ||
Theorem | snexg 5431 | A singleton built on a set is a set. Special case of snex 5432 which does not require ax-nul 5307 and is intuitionistically valid. (Contributed by NM, 7-Aug-1994.) (Revised by Mario Carneiro, 19-May-2013.) Extract from snex 5432 and shorten proof. (Revised by BJ, 15-Jan-2025.) |
⊢ (𝐴 ∈ 𝑉 → {𝐴} ∈ V) | ||
Theorem | snex 5432 | A singleton is a set. Theorem 7.12 of [Quine] p. 51, proved using Extensionality, Separation, Null Set, and Pairing. See also snexALT 5382. (Contributed by NM, 7-Aug-1994.) (Revised by Mario Carneiro, 19-May-2013.) |
⊢ {𝐴} ∈ V | ||
Theorem | prex 5433 | The Axiom of Pairing using class variables. Theorem 7.13 of [Quine] p. 51. By virtue of its definition, an unordered pair remains a set (even though no longer a pair) even when its components are proper classes (see prprc 4772), so we can dispense with hypotheses requiring them to be sets. (Contributed by NM, 15-Jul-1993.) |
⊢ {𝐴, 𝐵} ∈ V | ||
Theorem | exel 5434* |
There exist two sets, one a member of the other.
This theorem looks similar to el 5438, but its meaning is different. It only depends on the axioms ax-mp 5 to ax-4 1812, ax-6 1972, and ax-pr 5428. This theorem does not exclude that these two sets could actually be one single set containing itself. That two different sets exist is proved by exexneq 5435. (Contributed by SN, 23-Dec-2024.) |
⊢ ∃𝑦∃𝑥 𝑥 ∈ 𝑦 | ||
Theorem | exexneq 5435* | There exist two different sets. (Contributed by NM, 7-Nov-2006.) Avoid ax-13 2372. (Revised by BJ, 31-May-2019.) Avoid ax-8 2109. (Revised by SN, 21-Sep-2023.) Avoid ax-12 2172. (Revised by Rohan Ridenour, 9-Oct-2024.) Use ax-pr 5428 instead of ax-pow 5364. (Revised by BTernaryTau, 3-Dec-2024.) Extract this result from the proof of dtru 5437. (Revised by BJ, 2-Jan-2025.) |
⊢ ∃𝑥∃𝑦 ¬ 𝑥 = 𝑦 | ||
Theorem | exneq 5436* |
Given any set (the "𝑦 " in the statement), there
exists a set not
equal to it.
The same statement without disjoint variable condition is false, since we do not have ∃𝑥¬ 𝑥 = 𝑥. This theorem is proved directly from set theory axioms (no class definitions) and does not depend on ax-ext 2704, ax-sep 5300, or ax-pow 5364 nor auxiliary logical axiom schemes ax-10 2138 to ax-13 2372. See dtruALT 5387 for a shorter proof using more axioms, and dtruALT2 5369 for a proof using ax-pow 5364 instead of ax-pr 5428. (Contributed by NM, 7-Nov-2006.) Avoid ax-13 2372. (Revised by BJ, 31-May-2019.) Avoid ax-8 2109. (Revised by SN, 21-Sep-2023.) Avoid ax-12 2172. (Revised by Rohan Ridenour, 9-Oct-2024.) Use ax-pr 5428 instead of ax-pow 5364. (Revised by BTernaryTau, 3-Dec-2024.) Extract this result from the proof of dtru 5437. (Revised by BJ, 2-Jan-2025.) |
⊢ ∃𝑥 ¬ 𝑥 = 𝑦 | ||
Theorem | dtru 5437* | Given any set (the "𝑦 " in the statement), not all sets are equal to it. The same statement without disjoint variable condition is false since it contradicts stdpc6 2032. The same comments and revision history concerning axiom usage as in exneq 5436 apply. (Contributed by NM, 7-Nov-2006.) Extract exneq 5436 as an intermediate result. (Revised by BJ, 2-Jan-2025.) |
⊢ ¬ ∀𝑥 𝑥 = 𝑦 | ||
Theorem | el 5438* | Any set is an element of some other set. See elALT 5441 for a shorter proof using more axioms, and see elALT2 5368 for a proof that uses ax-9 2117 and ax-pow 5364 instead of ax-pr 5428. (Contributed by NM, 4-Jan-2002.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) Use ax-pr 5428 instead of ax-9 2117 and ax-pow 5364. (Revised by BTernaryTau, 2-Dec-2024.) |
⊢ ∃𝑦 𝑥 ∈ 𝑦 | ||
Theorem | sels 5439* | If a class is a set, then it is a member of a set. (Contributed by NM, 4-Jan-2002.) Generalize from the proof of elALT 5441. (Revised by BJ, 3-Apr-2019.) Avoid ax-sep 5300, ax-nul 5307, ax-pow 5364. (Revised by BTernaryTau, 15-Jan-2025.) |
⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝐴 ∈ 𝑥) | ||
Theorem | selsALT 5440* | Alternate proof of sels 5439, requiring ax-sep 5300 but not using el 5438 (which is proved from it as elALT 5441). (especially when the proof of el 5438 is inlined in sels 5439). (Contributed by NM, 4-Jan-2002.) Generalize from the proof of elALT 5441. (Revised by BJ, 3-Apr-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝐴 ∈ 𝑥) | ||
Theorem | elALT 5441* | Alternate proof of el 5438, shorter but requiring ax-sep 5300. (Contributed by NM, 4-Jan-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ∃𝑦 𝑥 ∈ 𝑦 | ||
Theorem | dtruOLD 5442* | Obsolete proof of dtru 5437 as of 01-Jan-2025. (Contributed by NM, 7-Nov-2006.) Avoid ax-13 2372. (Revised by BJ, 31-May-2019.) Avoid ax-12 2172. (Revised by Rohan Ridenour, 9-Oct-2024.) Use ax-pr 5428 instead of ax-pow 5364. (Revised by BTernaryTau, 3-Dec-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ¬ ∀𝑥 𝑥 = 𝑦 | ||
Theorem | snelpwg 5443 | A singleton of a set is a member of the powerclass of a class if and only if that set is a member of that class. (Contributed by NM, 1-Apr-1998.) Put in closed form and avoid ax-nul 5307. (Revised by BJ, 17-Jan-2025.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ {𝐴} ∈ 𝒫 𝐵)) | ||
Theorem | snelpwi 5444 | If a set is a member of a class, then the singleton of that set is a member of the powerclass of that class. (Contributed by Alan Sare, 25-Aug-2011.) |
⊢ (𝐴 ∈ 𝐵 → {𝐴} ∈ 𝒫 𝐵) | ||
Theorem | snelpwiOLD 5445 | Obsolete version of snelpwi 5444 as of 17-Jan-2025. (Contributed by NM, 28-May-1995.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 ∈ 𝐵 → {𝐴} ∈ 𝒫 𝐵) | ||
Theorem | snelpw 5446 | A singleton of a set is a member of the powerclass of a class if and only if that set is a member of that class. (Contributed by NM, 1-Apr-1998.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ 𝐵 ↔ {𝐴} ∈ 𝒫 𝐵) | ||
Theorem | prelpw 5447 | An unordered pair of two sets is a member of the powerclass of a class if and only if the two sets are members of that class. (Contributed by AV, 8-Jan-2020.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ↔ {𝐴, 𝐵} ∈ 𝒫 𝐶)) | ||
Theorem | prelpwi 5448 | If two sets are members of a class, then the unordered pair of those two sets is a member of the powerclass of that class. (Contributed by Thierry Arnoux, 10-Mar-2017.) (Proof shortened by AV, 23-Oct-2021.) |
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → {𝐴, 𝐵} ∈ 𝒫 𝐶) | ||
Theorem | rext 5449* | A theorem similar to extensionality, requiring the existence of a singleton. Exercise 8 of [TakeutiZaring] p. 16. (Contributed by NM, 10-Aug-1993.) |
⊢ (∀𝑧(𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧) → 𝑥 = 𝑦) | ||
Theorem | sspwb 5450 | The powerclass construction preserves and reflects inclusion. Classes are subclasses if and only if their power classes are subclasses. Exercise 18 of [TakeutiZaring] p. 18. (Contributed by NM, 13-Oct-1996.) |
⊢ (𝐴 ⊆ 𝐵 ↔ 𝒫 𝐴 ⊆ 𝒫 𝐵) | ||
Theorem | unipw 5451 | A class equals the union of its power class. Exercise 6(a) of [Enderton] p. 38. (Contributed by NM, 14-Oct-1996.) (Proof shortened by Alan Sare, 28-Dec-2008.) |
⊢ ∪ 𝒫 𝐴 = 𝐴 | ||
Theorem | univ 5452 | The union of the universe is the universe. Exercise 4.12(c) of [Mendelson] p. 235. (Contributed by NM, 14-Sep-2003.) |
⊢ ∪ V = V | ||
Theorem | pwtr 5453 | A class is transitive iff its power class is transitive. (Contributed by Alan Sare, 25-Aug-2011.) (Revised by Mario Carneiro, 15-Jun-2014.) |
⊢ (Tr 𝐴 ↔ Tr 𝒫 𝐴) | ||
Theorem | ssextss 5454* | An extensionality-like principle defining subclass in terms of subsets. (Contributed by NM, 30-Jun-2004.) |
⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ⊆ 𝐴 → 𝑥 ⊆ 𝐵)) | ||
Theorem | ssext 5455* | An extensionality-like principle that uses the subset instead of the membership relation: two classes are equal iff they have the same subsets. (Contributed by NM, 30-Jun-2004.) |
⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ⊆ 𝐴 ↔ 𝑥 ⊆ 𝐵)) | ||
Theorem | nssss 5456* | Negation of subclass relationship. Compare nss 4047. (Contributed by NM, 30-Jun-2004.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
⊢ (¬ 𝐴 ⊆ 𝐵 ↔ ∃𝑥(𝑥 ⊆ 𝐴 ∧ ¬ 𝑥 ⊆ 𝐵)) | ||
Theorem | pweqb 5457 | Classes are equal if and only if their power classes are equal. Exercise 19 of [TakeutiZaring] p. 18. (Contributed by NM, 13-Oct-1996.) |
⊢ (𝐴 = 𝐵 ↔ 𝒫 𝐴 = 𝒫 𝐵) | ||
Theorem | intidg 5458* | The intersection of all sets to which a set belongs is the singleton of that set. (Contributed by NM, 5-Jun-2009.) Put in closed form and avoid ax-nul 5307. (Revised by BJ, 17-Jan-2025.) |
⊢ (𝐴 ∈ 𝑉 → ∩ {𝑥 ∣ 𝐴 ∈ 𝑥} = {𝐴}) | ||
Theorem | intidOLD 5459* | Obsolete version of intidg 5458 as of 18-Jan-2025. (Contributed by NM, 5-Jun-2009.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝐴 ∈ V ⇒ ⊢ ∩ {𝑥 ∣ 𝐴 ∈ 𝑥} = {𝐴} | ||
Theorem | moabex 5460 | "At most one" existence implies a class abstraction exists. (Contributed by NM, 30-Dec-1996.) |
⊢ (∃*𝑥𝜑 → {𝑥 ∣ 𝜑} ∈ V) | ||
Theorem | rmorabex 5461 | Restricted "at most one" existence implies a restricted class abstraction exists. (Contributed by NM, 17-Jun-2017.) |
⊢ (∃*𝑥 ∈ 𝐴 𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ V) | ||
Theorem | euabex 5462 | The abstraction of a wff with existential uniqueness exists. (Contributed by NM, 25-Nov-1994.) |
⊢ (∃!𝑥𝜑 → {𝑥 ∣ 𝜑} ∈ V) | ||
Theorem | nnullss 5463* | A nonempty class (even if proper) has a nonempty subset. (Contributed by NM, 23-Aug-2003.) |
⊢ (𝐴 ≠ ∅ → ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅)) | ||
Theorem | exss 5464* | Restricted existence in a class (even if proper) implies restricted existence in a subset. (Contributed by NM, 23-Aug-2003.) |
⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑦(𝑦 ⊆ 𝐴 ∧ ∃𝑥 ∈ 𝑦 𝜑)) | ||
Theorem | opex 5465 | An ordered pair of classes is a set. Exercise 7 of [TakeutiZaring] p. 16. (Contributed by NM, 18-Aug-1993.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ ⟨𝐴, 𝐵⟩ ∈ V | ||
Theorem | otex 5466 | An ordered triple of classes is a set. (Contributed by NM, 3-Apr-2015.) |
⊢ ⟨𝐴, 𝐵, 𝐶⟩ ∈ V | ||
Theorem | elopg 5467 | Characterization of the elements of an ordered pair. Closed form of elop 5468. (Contributed by BJ, 22-Jun-2019.) (Avoid depending on this detail.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶 ∈ ⟨𝐴, 𝐵⟩ ↔ (𝐶 = {𝐴} ∨ 𝐶 = {𝐴, 𝐵}))) | ||
Theorem | elop 5468 | Characterization of the elements of an ordered pair. Exercise 3 of [TakeutiZaring] p. 15. (Contributed by NM, 15-Jul-1993.) (Revised by Mario Carneiro, 26-Apr-2015.) Remove an extraneous hypothesis. (Revised by BJ, 25-Dec-2020.) (Avoid depending on this detail.) |
⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V ⇒ ⊢ (𝐴 ∈ ⟨𝐵, 𝐶⟩ ↔ (𝐴 = {𝐵} ∨ 𝐴 = {𝐵, 𝐶})) | ||
Theorem | opi1 5469 | One of the two elements in an ordered pair. (Contributed by NM, 15-Jul-1993.) (Revised by Mario Carneiro, 26-Apr-2015.) (Avoid depending on this detail.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ {𝐴} ∈ ⟨𝐴, 𝐵⟩ | ||
Theorem | opi2 5470 | One of the two elements of an ordered pair. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 26-Apr-2015.) (Avoid depending on this detail.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ {𝐴, 𝐵} ∈ ⟨𝐴, 𝐵⟩ | ||
Theorem | opeluu 5471 | Each member of an ordered pair belongs to the union of the union of a class to which the ordered pair belongs. Lemma 3D of [Enderton] p. 41. (Contributed by NM, 31-Mar-1995.) (Revised by Mario Carneiro, 27-Feb-2016.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (⟨𝐴, 𝐵⟩ ∈ 𝐶 → (𝐴 ∈ ∪ ∪ 𝐶 ∧ 𝐵 ∈ ∪ ∪ 𝐶)) | ||
Theorem | op1stb 5472 | Extract the first member of an ordered pair. Theorem 73 of [Suppes] p. 42. (See op2ndb 6227 to extract the second member, op1sta 6225 for an alternate version, and op1st 7983 for the preferred version.) (Contributed by NM, 25-Nov-2003.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ∩ ∩ ⟨𝐴, 𝐵⟩ = 𝐴 | ||
Theorem | brv 5473 | Two classes are always in relation by V. This is simply equivalent to ⟨𝐴, 𝐵⟩ ∈ V, and does not imply that V is a relation: see nrelv 5801. (Contributed by Scott Fenton, 11-Apr-2012.) |
⊢ 𝐴V𝐵 | ||
Theorem | opnz 5474 | An ordered pair is nonempty iff the arguments are sets. (Contributed by NM, 24-Jan-2004.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ (⟨𝐴, 𝐵⟩ ≠ ∅ ↔ (𝐴 ∈ V ∧ 𝐵 ∈ V)) | ||
Theorem | opnzi 5475 | An ordered pair is nonempty if the arguments are sets. (Contributed by Mario Carneiro, 26-Apr-2015.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ⟨𝐴, 𝐵⟩ ≠ ∅ | ||
Theorem | opth1 5476 | Equality of the first members of equal ordered pairs. (Contributed by NM, 28-May-2008.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → 𝐴 = 𝐶) | ||
Theorem | opth 5477 | The ordered pair theorem. If two ordered pairs are equal, their first elements are equal and their second elements are equal. Exercise 6 of [TakeutiZaring] p. 16. Note that 𝐶 and 𝐷 are not required to be sets due our specific ordered pair definition. (Contributed by NM, 28-May-1995.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) | ||
Theorem | opthg 5478 | Ordered pair theorem. 𝐶 and 𝐷 are not required to be sets under our specific ordered pair definition. (Contributed by NM, 14-Oct-2005.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))) | ||
Theorem | opth1g 5479 | Equality of the first members of equal ordered pairs. Closed form of opth1 5476. (Contributed by AV, 14-Oct-2018.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → 𝐴 = 𝐶)) | ||
Theorem | opthg2 5480 | Ordered pair theorem. (Contributed by NM, 14-Oct-2005.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ ((𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊) → (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))) | ||
Theorem | opth2 5481 | Ordered pair theorem. (Contributed by NM, 21-Sep-2014.) |
⊢ 𝐶 ∈ V & ⊢ 𝐷 ∈ V ⇒ ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) | ||
Theorem | opthneg 5482 | Two ordered pairs are not equal iff their first components or their second components are not equal. (Contributed by AV, 13-Dec-2018.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (⟨𝐴, 𝐵⟩ ≠ ⟨𝐶, 𝐷⟩ ↔ (𝐴 ≠ 𝐶 ∨ 𝐵 ≠ 𝐷))) | ||
Theorem | opthne 5483 | Two ordered pairs are not equal iff their first components or their second components are not equal. (Contributed by AV, 13-Dec-2018.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (⟨𝐴, 𝐵⟩ ≠ ⟨𝐶, 𝐷⟩ ↔ (𝐴 ≠ 𝐶 ∨ 𝐵 ≠ 𝐷)) | ||
Theorem | otth2 5484 | Ordered triple theorem, with triple expressed with ordered pairs. (Contributed by NM, 1-May-1995.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝑅 ∈ V ⇒ ⊢ (⟨⟨𝐴, 𝐵⟩, 𝑅⟩ = ⟨⟨𝐶, 𝐷⟩, 𝑆⟩ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ∧ 𝑅 = 𝑆)) | ||
Theorem | otth 5485 | Ordered triple theorem. (Contributed by NM, 25-Sep-2014.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝑅 ∈ V ⇒ ⊢ (⟨𝐴, 𝐵, 𝑅⟩ = ⟨𝐶, 𝐷, 𝑆⟩ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ∧ 𝑅 = 𝑆)) | ||
Theorem | otthg 5486 | Ordered triple theorem, closed form. (Contributed by Alexander van der Vekens, 10-Mar-2018.) |
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝐷, 𝐸, 𝐹⟩ ↔ (𝐴 = 𝐷 ∧ 𝐵 = 𝐸 ∧ 𝐶 = 𝐹))) | ||
Theorem | otthne 5487 | Contrapositive of the ordered triple theorem. (Contributed by Scott Fenton, 31-Jan-2025.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V ⇒ ⊢ (⟨𝐴, 𝐵, 𝐶⟩ ≠ ⟨𝐷, 𝐸, 𝐹⟩ ↔ (𝐴 ≠ 𝐷 ∨ 𝐵 ≠ 𝐸 ∨ 𝐶 ≠ 𝐹)) | ||
Theorem | eqvinop 5488* | A variable introduction law for ordered pairs. Analogue of Lemma 15 of [Monk2] p. 109. (Contributed by NM, 28-May-1995.) |
⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V ⇒ ⊢ (𝐴 = ⟨𝐵, 𝐶⟩ ↔ ∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ ⟨𝑥, 𝑦⟩ = ⟨𝐵, 𝐶⟩)) | ||
Theorem | sbcop1 5489* | The proper substitution of an ordered pair for a setvar variable corresponds to a proper substitution of its first component. (Contributed by AV, 8-Apr-2023.) |
⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ 𝜓)) ⇒ ⊢ ([𝑎 / 𝑥]𝜓 ↔ [⟨𝑎, 𝑦⟩ / 𝑧]𝜑) | ||
Theorem | sbcop 5490* | The proper substitution of an ordered pair for a setvar variable corresponds to a proper substitution of each of its components. (Contributed by AV, 8-Apr-2023.) |
⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ 𝜓)) ⇒ ⊢ ([𝑏 / 𝑦][𝑎 / 𝑥]𝜓 ↔ [⟨𝑎, 𝑏⟩ / 𝑧]𝜑) | ||
Theorem | copsexgw 5491* | Version of copsexg 5492 with a disjoint variable condition, which does not require ax-13 2372. (Contributed by Gino Giotto, 26-Jan-2024.) |
⊢ (𝐴 = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ ∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑))) | ||
Theorem | copsexg 5492* | Substitution of class 𝐴 for ordered pair ⟨𝑥, 𝑦⟩. Usage of this theorem is discouraged because it depends on ax-13 2372. Use the weaker copsexgw 5491 when possible. (Contributed by NM, 27-Dec-1996.) (Revised by Andrew Salmon, 11-Jul-2011.) (Proof shortened by Wolf Lammen, 25-Aug-2019.) (New usage is discouraged.) |
⊢ (𝐴 = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ ∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑))) | ||
Theorem | copsex2t 5493* | Closed theorem form of copsex2g 5494. (Contributed by NM, 17-Feb-2013.) |
⊢ ((∀𝑥∀𝑦((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊)) → (∃𝑥∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ 𝜓)) | ||
Theorem | copsex2g 5494* | Implicit substitution inference for ordered pairs. (Contributed by NM, 28-May-1995.) Use a similar proof to copsex4g 5496 to reduce axiom usage. (Revised by SN, 1-Sep-2024.) |
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∃𝑥∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ 𝜓)) | ||
Theorem | copsex2gOLD 5495* | Obsolete version of copsex2g 5494 as of 1-Sep-2024. (Contributed by NM, 28-May-1995.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∃𝑥∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ 𝜓)) | ||
Theorem | copsex4g 5496* | An implicit substitution inference for 2 ordered pairs. (Contributed by NM, 5-Aug-1995.) |
⊢ (((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑤 = 𝐷)) → (𝜑 ↔ 𝜓)) ⇒ ⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑅 ∧ 𝐷 ∈ 𝑆)) → (∃𝑥∃𝑦∃𝑧∃𝑤((⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑧, 𝑤⟩) ∧ 𝜑) ↔ 𝜓)) | ||
Theorem | 0nelop 5497 | A property of ordered pairs. (Contributed by Mario Carneiro, 26-Apr-2015.) |
⊢ ¬ ∅ ∈ ⟨𝐴, 𝐵⟩ | ||
Theorem | opwo0id 5498 | An ordered pair is equal to the ordered pair without the empty set. This is because no ordered pair contains the empty set. (Contributed by AV, 15-Nov-2021.) |
⊢ ⟨𝑋, 𝑌⟩ = (⟨𝑋, 𝑌⟩ ∖ {∅}) | ||
Theorem | opeqex 5499 | Equivalence of existence implied by equality of ordered pairs. (Contributed by NM, 28-May-2008.) |
⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → ((𝐴 ∈ V ∧ 𝐵 ∈ V) ↔ (𝐶 ∈ V ∧ 𝐷 ∈ V))) | ||
Theorem | oteqex2 5500 | Equivalence of existence implied by equality of ordered triples. (Contributed by NM, 26-Apr-2015.) |
⊢ (⟨⟨𝐴, 𝐵⟩, 𝐶⟩ = ⟨⟨𝑅, 𝑆⟩, 𝑇⟩ → (𝐶 ∈ V ↔ 𝑇 ∈ V)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |