![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > rexbidv2 | Structured version Visualization version GIF version |
Description: Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 22-May-1999.) |
Ref | Expression |
---|---|
rexbidv2.1 | ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐵 ∧ 𝜒))) |
Ref | Expression |
---|---|
rexbidv2 | ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rexbidv2.1 | . . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐵 ∧ 𝜒))) | |
2 | 1 | exbidv 1919 | . 2 ⊢ (𝜑 → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜓) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜒))) |
3 | df-rex 3069 | . 2 ⊢ (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜓)) | |
4 | df-rex 3069 | . 2 ⊢ (∃𝑥 ∈ 𝐵 𝜒 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜒)) | |
5 | 2, 3, 4 | 3bitr4g 314 | 1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∃wex 1776 ∈ wcel 2106 ∃wrex 3068 |
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 1908 |
This theorem depends on definitions: df-bi 207 df-ex 1777 df-rex 3069 |
This theorem is referenced by: rexbidva 3175 rexeqbidv 3345 rexss 4071 iuneq12d 5026 exopxfr2 5858 isoini 7358 rexsupp 8206 omabs 8688 elfi2 9452 wemapsolem 9588 ltexpi 10940 rexuz 12938 ncoprmgcdne1b 16684 lpigen 21363 llyi 23498 nllyi 23499 elpi1 25092 ressupprn 32705 xrecex 32887 bnj18eq1 34920 ldual1dim 39148 pmapjat1 39836 mrefg2 42695 islssfg2 43060 fourierdlem71 46133 hoiqssbl 46581 reuxfr1dd 48655 lubeldm2d 48755 glbeldm2d 48756 |
Copyright terms: Public domain | W3C validator |