Users' Mathboxes Mathbox for BJ < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bj-bm1.3ii Structured version   Visualization version   GIF version

Theorem bj-bm1.3ii 35231
Description: The extension of a predicate (𝜑(𝑧)) is included in a set (𝑥) if and only if it is a set (𝑦). Sufficiency is obvious, and necessity is the content of the axiom of separation ax-sep 5227. Similar to Theorem 1.3(ii) of [BellMachover] p. 463. (Contributed by NM, 21-Jun-1993.) Generalized to a closed form biconditional with existential quantifications using two different setvars 𝑥, 𝑦 (which need not be disjoint). (Revised by BJ, 8-Aug-2022.)

TODO: move in place of bm1.3ii 5230. Relabel ("sepbi"?).

Assertion
Ref Expression
bj-bm1.3ii (∃𝑥𝑧(𝜑𝑧𝑥) ↔ ∃𝑦𝑧(𝑧𝑦𝜑))
Distinct variable groups:   𝑥,𝑧   𝑦,𝑧   𝜑,𝑥   𝜑,𝑦
Allowed substitution hint:   𝜑(𝑧)

Proof of Theorem bj-bm1.3ii
Dummy variable 𝑡 is distinct from all other variables.
StepHypRef Expression
1 elequ2 2125 . . . . 5 (𝑥 = 𝑡 → (𝑧𝑥𝑧𝑡))
21imbi2d 341 . . . 4 (𝑥 = 𝑡 → ((𝜑𝑧𝑥) ↔ (𝜑𝑧𝑡)))
32albidv 1927 . . 3 (𝑥 = 𝑡 → (∀𝑧(𝜑𝑧𝑥) ↔ ∀𝑧(𝜑𝑧𝑡)))
43cbvexvw 2044 . 2 (∃𝑥𝑧(𝜑𝑧𝑥) ↔ ∃𝑡𝑧(𝜑𝑧𝑡))
5 ax-sep 5227 . . . . 5 𝑦𝑧(𝑧𝑦 ↔ (𝑧𝑡𝜑))
6 19.42v 1961 . . . . . 6 (∃𝑦(∀𝑧(𝜑𝑧𝑡) ∧ ∀𝑧(𝑧𝑦 ↔ (𝑧𝑡𝜑))) ↔ (∀𝑧(𝜑𝑧𝑡) ∧ ∃𝑦𝑧(𝑧𝑦 ↔ (𝑧𝑡𝜑))))
7 bimsc1 841 . . . . . . . 8 (((𝜑𝑧𝑡) ∧ (𝑧𝑦 ↔ (𝑧𝑡𝜑))) → (𝑧𝑦𝜑))
87alanimi 1823 . . . . . . 7 ((∀𝑧(𝜑𝑧𝑡) ∧ ∀𝑧(𝑧𝑦 ↔ (𝑧𝑡𝜑))) → ∀𝑧(𝑧𝑦𝜑))
98eximi 1841 . . . . . 6 (∃𝑦(∀𝑧(𝜑𝑧𝑡) ∧ ∀𝑧(𝑧𝑦 ↔ (𝑧𝑡𝜑))) → ∃𝑦𝑧(𝑧𝑦𝜑))
106, 9sylbir 234 . . . . 5 ((∀𝑧(𝜑𝑧𝑡) ∧ ∃𝑦𝑧(𝑧𝑦 ↔ (𝑧𝑡𝜑))) → ∃𝑦𝑧(𝑧𝑦𝜑))
115, 10mpan2 688 . . . 4 (∀𝑧(𝜑𝑧𝑡) → ∃𝑦𝑧(𝑧𝑦𝜑))
1211exlimiv 1937 . . 3 (∃𝑡𝑧(𝜑𝑧𝑡) → ∃𝑦𝑧(𝑧𝑦𝜑))
13 elequ2 2125 . . . . . . 7 (𝑦 = 𝑡 → (𝑧𝑦𝑧𝑡))
1413bibi1d 344 . . . . . 6 (𝑦 = 𝑡 → ((𝑧𝑦𝜑) ↔ (𝑧𝑡𝜑)))
1514albidv 1927 . . . . 5 (𝑦 = 𝑡 → (∀𝑧(𝑧𝑦𝜑) ↔ ∀𝑧(𝑧𝑡𝜑)))
1615cbvexvw 2044 . . . 4 (∃𝑦𝑧(𝑧𝑦𝜑) ↔ ∃𝑡𝑧(𝑧𝑡𝜑))
17 biimpr 219 . . . . . 6 ((𝑧𝑡𝜑) → (𝜑𝑧𝑡))
1817alimi 1818 . . . . 5 (∀𝑧(𝑧𝑡𝜑) → ∀𝑧(𝜑𝑧𝑡))
1918eximi 1841 . . . 4 (∃𝑡𝑧(𝑧𝑡𝜑) → ∃𝑡𝑧(𝜑𝑧𝑡))
2016, 19sylbi 216 . . 3 (∃𝑦𝑧(𝑧𝑦𝜑) → ∃𝑡𝑧(𝜑𝑧𝑡))
2112, 20impbii 208 . 2 (∃𝑡𝑧(𝜑𝑧𝑡) ↔ ∃𝑦𝑧(𝑧𝑦𝜑))
224, 21bitri 274 1 (∃𝑥𝑧(𝜑𝑧𝑥) ↔ ∃𝑦𝑧(𝑧𝑦𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  wal 1540  wex 1786
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-9 2120  ax-sep 5227
This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1787
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator