| 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 uniqueness 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 579 | . . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐴 ∧ 𝜒))) |
| 3 | 2 | eubidv 2586 | . 2 ⊢ (𝜑 → (∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜓) ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜒))) |
| 4 | df-reu 3381 | . 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜓)) | |
| 5 | df-reu 3381 | . 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜒 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜒)) | |
| 6 | 3, 4, 5 | 3bitr4g 314 | 1 ⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐴 𝜒)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∈ wcel 2108 ∃!weu 2568 ∃!wreu 3378 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-mo 2540 df-eu 2569 df-reu 3381 |
| This theorem is referenced by: reubidv 3398 reuxfrd 3754 reuxfr1d 3756 fdmeu 6965 exfo 7125 f1ofveu 7425 zmax 12987 zbtwnre 12988 rebtwnz 12989 icoshftf1o 13514 divalgb 16441 1arith2 16966 ply1divalg2 26178 addsq2reu 27484 addsqn2reu 27485 addsqrexnreu 27486 2sqreultlem 27491 2sqreunnltlem 27494 frgr2wwlkeu 30346 numclwwlk2lem1 30395 numclwlk2lem2f1o 30398 pjhtheu2 31435 reuxfrdf 32510 xrsclat 33013 xrmulc1cn 33929 ply1divalg3 35647 poimirlem25 37652 hdmap14lem14 41883 cantnf2 43338 prproropreud 47496 quad1 47607 requad1 47609 requad2 47610 isuspgrim0lem 47871 isuspgrim0 47872 isuspgrimlem 47874 itscnhlinecirc02p 48706 reuxfr1dd 48726 |
| Copyright terms: Public domain | W3C validator |