Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > reubidva | Structured version Visualization version GIF version |
Description: Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 13-Nov-2004.) Reduce axiom usage. (Revised by Wolf Lammen, 14-Jan-2023.) |
Ref | Expression |
---|---|
reubidva.1 | ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
reubidva | ⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐴 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | reubidva.1 | . . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) | |
2 | 1 | pm5.32da 582 | . . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐴 ∧ 𝜒))) |
3 | 2 | eubidv 2647 | . 2 ⊢ (𝜑 → (∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜓) ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜒))) |
4 | df-reu 3113 | . 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜓)) | |
5 | df-reu 3113 | . 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜒 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜒)) | |
6 | 3, 4, 5 | 3bitr4g 317 | 1 ⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐴 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 ∈ wcel 2111 ∃!weu 2628 ∃!wreu 3108 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 |
This theorem depends on definitions: df-bi 210 df-an 400 df-ex 1782 df-mo 2598 df-eu 2629 df-reu 3113 |
This theorem is referenced by: reubidv 3342 reuxfrd 3687 reuxfr1d 3689 exfo 6848 f1ofveu 7130 zmax 12333 zbtwnre 12334 rebtwnz 12335 icoshftf1o 12852 divalgb 15745 1arith2 16254 ply1divalg2 24739 addsq2reu 26024 addsqn2reu 26025 addsqrexnreu 26026 2sqreultlem 26031 2sqreunnltlem 26034 frgr2wwlkeu 28112 numclwwlk2lem1 28161 numclwlk2lem2f1o 28164 pjhtheu2 29199 reuxfrdf 30262 xrsclat 30714 xrmulc1cn 31283 poimirlem25 35082 hdmap14lem14 39177 prproropreud 44026 quad1 44138 requad1 44140 requad2 44141 itscnhlinecirc02p 45199 |
Copyright terms: Public domain | W3C validator |