![]() |
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 579 | . . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐴 ∧ 𝜒))) |
3 | 2 | eubidv 2580 | . 2 ⊢ (𝜑 → (∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜓) ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜒))) |
4 | df-reu 3377 | . 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜓)) | |
5 | df-reu 3377 | . 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜒 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜒)) | |
6 | 3, 4, 5 | 3bitr4g 313 | 1 ⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐴 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 ∈ wcel 2106 ∃!weu 2562 ∃!wreu 3374 |
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 1913 |
This theorem depends on definitions: df-bi 206 df-an 397 df-ex 1782 df-mo 2534 df-eu 2563 df-reu 3377 |
This theorem is referenced by: reubidv 3394 reuxfrd 3744 reuxfr1d 3746 exfo 7106 f1ofveu 7405 zmax 12931 zbtwnre 12932 rebtwnz 12933 icoshftf1o 13453 divalgb 16349 1arith2 16863 ply1divalg2 25663 addsq2reu 26950 addsqn2reu 26951 addsqrexnreu 26952 2sqreultlem 26957 2sqreunnltlem 26960 frgr2wwlkeu 29618 numclwwlk2lem1 29667 numclwlk2lem2f1o 29670 pjhtheu2 30707 reuxfrdf 31769 xrsclat 32219 xrmulc1cn 32979 poimirlem25 36599 hdmap14lem14 40838 cantnf2 42157 prproropreud 46256 quad1 46367 requad1 46369 requad2 46370 itscnhlinecirc02p 47549 |
Copyright terms: Public domain | W3C validator |