![]() |
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 |
---|---|
rmobidva.1 | ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
reubidva | ⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐴 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rmobidva.1 | . . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) | |
2 | 1 | pm5.32da 578 | . . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐴 ∧ 𝜒))) |
3 | 2 | eubidv 2579 | . 2 ⊢ (𝜑 → (∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜓) ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜒))) |
4 | df-reu 3376 | . 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜓)) | |
5 | df-reu 3376 | . 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜒 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜒)) | |
6 | 3, 4, 5 | 3bitr4g 314 | 1 ⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐴 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 395 ∈ wcel 2105 ∃!weu 2561 ∃!wreu 3373 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 |
This theorem depends on definitions: df-bi 206 df-an 396 df-ex 1781 df-mo 2533 df-eu 2562 df-reu 3376 |
This theorem is referenced by: reubidv 3393 reuxfrd 3744 reuxfr1d 3746 exfo 7106 f1ofveu 7406 zmax 12934 zbtwnre 12935 rebtwnz 12936 icoshftf1o 13456 divalgb 16352 1arith2 16866 ply1divalg2 25892 addsq2reu 27180 addsqn2reu 27181 addsqrexnreu 27182 2sqreultlem 27187 2sqreunnltlem 27190 frgr2wwlkeu 29848 numclwwlk2lem1 29897 numclwlk2lem2f1o 29900 pjhtheu2 30937 reuxfrdf 31999 xrsclat 32449 xrmulc1cn 33209 poimirlem25 36817 hdmap14lem14 41056 cantnf2 42378 prproropreud 46476 quad1 46587 requad1 46589 requad2 46590 itscnhlinecirc02p 47559 |
Copyright terms: Public domain | W3C validator |