Metamath Proof Explorer

Theorem bj-fvimacnv0

Description: Variant of fvimacnv where membership of A in the domain is not needed provided the containing class B does not contain the empty set. Note that this antecedent would not be needed with Definition df-afv . (Contributed by BJ, 7-Jan-2024)

Ref Expression
Assertion bj-fvimacnv0 ⊢ Fun ⁡ F ∧ ¬ ∅ ∈ B → F ⁡ A ∈ B ↔ A ∈ F -1 B

Proof

Step Hyp Ref Expression
1 eleq1 ⊢ F ⁡ A = ∅ → F ⁡ A ∈ B ↔ ∅ ∈ B
2 1 biimpcd ⊢ F ⁡ A ∈ B → F ⁡ A = ∅ → ∅ ∈ B
3 2 con3rr3 ⊢ ¬ ∅ ∈ B → F ⁡ A ∈ B → ¬ F ⁡ A = ∅
4 3 imp ⊢ ¬ ∅ ∈ B ∧ F ⁡ A ∈ B → ¬ F ⁡ A = ∅
5 ndmfv ⊢ ¬ A ∈ dom ⁡ F → F ⁡ A = ∅
6 4 5 nsyl2 ⊢ ¬ ∅ ∈ B ∧ F ⁡ A ∈ B → A ∈ dom ⁡ F
7 simpr ⊢ ¬ ∅ ∈ B ∧ F ⁡ A ∈ B → F ⁡ A ∈ B
8 fvimacnv ⊢ Fun ⁡ F ∧ A ∈ dom ⁡ F → F ⁡ A ∈ B ↔ A ∈ F -1 B
9 8 biimpd ⊢ Fun ⁡ F ∧ A ∈ dom ⁡ F → F ⁡ A ∈ B → A ∈ F -1 B
10 9 ex ⊢ Fun ⁡ F → A ∈ dom ⁡ F → F ⁡ A ∈ B → A ∈ F -1 B
11 10 com3l ⊢ A ∈ dom ⁡ F → F ⁡ A ∈ B → Fun ⁡ F → A ∈ F -1 B
12 6 7 11 sylc ⊢ ¬ ∅ ∈ B ∧ F ⁡ A ∈ B → Fun ⁡ F → A ∈ F -1 B
13 12 ex ⊢ ¬ ∅ ∈ B → F ⁡ A ∈ B → Fun ⁡ F → A ∈ F -1 B
14 13 com3r ⊢ Fun ⁡ F → ¬ ∅ ∈ B → F ⁡ A ∈ B → A ∈ F -1 B
15 14 imp ⊢ Fun ⁡ F ∧ ¬ ∅ ∈ B → F ⁡ A ∈ B → A ∈ F -1 B
16 fvimacnvi ⊢ Fun ⁡ F ∧ A ∈ F -1 B → F ⁡ A ∈ B
17 16 ex ⊢ Fun ⁡ F → A ∈ F -1 B → F ⁡ A ∈ B
18 17 adantr ⊢ Fun ⁡ F ∧ ¬ ∅ ∈ B → A ∈ F -1 B → F ⁡ A ∈ B
19 15 18 impbid ⊢ Fun ⁡ F ∧ ¬ ∅ ∈ B → F ⁡ A ∈ B ↔ A ∈ F -1 B