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 34351
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 5195. 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 5198. 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 343 . . . 4 (𝑥 = 𝑡 → ((𝜑𝑧𝑥) ↔ (𝜑𝑧𝑡)))
32albidv 1917 . . 3 (𝑥 = 𝑡 → (∀𝑧(𝜑𝑧𝑥) ↔ ∀𝑧(𝜑𝑧𝑡)))
43cbvexvw 2040 . 2 (∃𝑥𝑧(𝜑𝑧𝑥) ↔ ∃𝑡𝑧(𝜑𝑧𝑡))
5 ax-sep 5195 . . . . 5 𝑦𝑧(𝑧𝑦 ↔ (𝑧𝑡𝜑))
6 19.42v 1950 . . . . . 6 (∃𝑦(∀𝑧(𝜑𝑧𝑡) ∧ ∀𝑧(𝑧𝑦 ↔ (𝑧𝑡𝜑))) ↔ (∀𝑧(𝜑𝑧𝑡) ∧ ∃𝑦𝑧(𝑧𝑦 ↔ (𝑧𝑡𝜑))))
7 bimsc1 840 . . . . . . . 8 (((𝜑𝑧𝑡) ∧ (𝑧𝑦 ↔ (𝑧𝑡𝜑))) → (𝑧𝑦𝜑))
87alanimi 1813 . . . . . . 7 ((∀𝑧(𝜑𝑧𝑡) ∧ ∀𝑧(𝑧𝑦 ↔ (𝑧𝑡𝜑))) → ∀𝑧(𝑧𝑦𝜑))
98eximi 1831 . . . . . 6 (∃𝑦(∀𝑧(𝜑𝑧𝑡) ∧ ∀𝑧(𝑧𝑦 ↔ (𝑧𝑡𝜑))) → ∃𝑦𝑧(𝑧𝑦𝜑))
106, 9sylbir 237 . . . . 5 ((∀𝑧(𝜑𝑧𝑡) ∧ ∃𝑦𝑧(𝑧𝑦 ↔ (𝑧𝑡𝜑))) → ∃𝑦𝑧(𝑧𝑦𝜑))
115, 10mpan2 689 . . . 4 (∀𝑧(𝜑𝑧𝑡) → ∃𝑦𝑧(𝑧𝑦𝜑))
1211exlimiv 1927 . . 3 (∃𝑡𝑧(𝜑𝑧𝑡) → ∃𝑦𝑧(𝑧𝑦𝜑))
13 elequ2 2125 . . . . . . 7 (𝑦 = 𝑡 → (𝑧𝑦𝑧𝑡))
1413bibi1d 346 . . . . . 6 (𝑦 = 𝑡 → ((𝑧𝑦𝜑) ↔ (𝑧𝑡𝜑)))
1514albidv 1917 . . . . 5 (𝑦 = 𝑡 → (∀𝑧(𝑧𝑦𝜑) ↔ ∀𝑧(𝑧𝑡𝜑)))
1615cbvexvw 2040 . . . 4 (∃𝑦𝑧(𝑧𝑦𝜑) ↔ ∃𝑡𝑧(𝑧𝑡𝜑))
17 biimpr 222 . . . . . 6 ((𝑧𝑡𝜑) → (𝜑𝑧𝑡))
1817alimi 1808 . . . . 5 (∀𝑧(𝑧𝑡𝜑) → ∀𝑧(𝜑𝑧𝑡))
1918eximi 1831 . . . 4 (∃𝑡𝑧(𝑧𝑡𝜑) → ∃𝑡𝑧(𝜑𝑧𝑡))
2016, 19sylbi 219 . . 3 (∃𝑦𝑧(𝑧𝑦𝜑) → ∃𝑡𝑧(𝜑𝑧𝑡))
2112, 20impbii 211 . 2 (∃𝑡𝑧(𝜑𝑧𝑡) ↔ ∃𝑦𝑧(𝑧𝑦𝜑))
224, 21bitri 277 1 (∃𝑥𝑧(𝜑𝑧𝑥) ↔ ∃𝑦𝑧(𝑧𝑦𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 208  wa 398  wal 1531  wex 1776
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-9 2120  ax-sep 5195
This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator